Recurrent bluescreens, program crashes, accidents and computer malfunctions are making us painfully aware that computer programming is difficult, and thus, program correctness is an inherent challenge of computer science. Program verification is a research field whose ultimate goal is to assert the correctness of a program with mathematical precision, i.e., by means of mathematical proof. Since programs can often be extremely large, it is not realistic for human engineers to construct proofs about programs by hand. Computer-aided verification therefore is using computers to prove the correctness of computer programs.
The PROSEED research project proposes an innovative approach to verification which is based on the insight that program texts are carrying important information which is directed at the human readers of the program. We will utilize this human engineering information in a logically sound framework for computer-aided verification.