ICT Call 2010ICT10-050

PROSEED: Proof Seeding for Software Verification


PROSEED: Proof Seeding for Software Verification
Principal Investigator:
Projekttitel:
PROSEED: Proof Seeding for Software Verification
Status:
Abgeschlossen (01.01.2011 – 31.12.2014) 48 Monate
Fördersumme:
€ 598.000

 
Kurzzusammenfassung:

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.

 

Wir nutzen Cookies auf unserer Website. Einige von ihnen sind technisch notwendig, während andere uns helfen, diese Website zu verbessern oder zusätzliche Funktionalitäten zur Verfügung zu stellen. Weitere Informationen