ICT Call 2010ICT10-050

PROSEED: Proof Seeding for Software Verification


PROSEED: Proof Seeding for Software Verification
Principal Investigator:
Project title:
PROSEED: Proof Seeding for Software Verification
Status:
Completed (01.01.2011 – 31.12.2014)
Funding volume:
€ 598,000

 
Abstract:

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.

 

We use cookies on our website. Some of them are technically necessary, while others help us to improve this website or provide additional functionalities. Further information