Gecertificeerde semi-automatische modulaire formele programma verificatie

Semi-automatische, modulaire, formele verificatie van broncode, op basis van annotaties, is een veelbelovende aanpak om veiligheids- en correctheidseigenschappen van programma's te verifiëren. Deze aanpak combineert hoge betrouwbaarheid met relatief goede bruikbaarheid voor ontwikkelaars, door het aanbieden van een debugger-achtige gebruikerservaring. In de huidige state of the art, zijn de formele verificatietools echter zelf nog niet geverifieerd om vrij te zijn van bugs. In dit doctoraatsproject ontwikkelen we een methode om deze semi-automatische formele verificatietools zodanig uit te breiden dat zij, bij succesvolle verificatie, een object genereren dat automatisch gecontroleerd kan worden en dat certificeert dat het input programma inderdaad aan de beloofde eigenschappen voldoet. Concreet zullen wij deze aanpak valideren door de VeriFast tool voor C programma's zo uit te breiden dat bij succesvolle verificatie Coq proof scripts worden genereert, op basis van een in Coq geformaliseerde semantiek van C (zoals CompCert of CH2O/Formalin).