Formal verification is an area of theoretical computer science where mathematical logic is used to prove that a program behaves in a certain way. With the methods in formal verification, you can prove that the program follows some given specification and thereby behaves in the desired way. The area is largely split up into two distinct parts. One deals with how the program transforms data. This uses Hoare logic and deductive verification to prove that the program follows a given specification. The other part deals with temporal properties of the program, this uses temporal logic and model checkers.

The two areas are today largely separated. This report builds on a framework by Alur and Chaudhuri [1] which proves temporal properties in a Hoare logic style reasoning. By using this framework, this report aims to check the viability of using it with deductive verifiers. Thereby bridging the gap between the two areas for formal verification.

In conclusion, the report finds that it is certainly possible to prove temporal properties for C programs using Alur and Chaudhuri’s framework with deductive verifiers. In practical terms, though, it requires too much work to be feasible to use this framework by manually creating annotations for the deductive verifiers. In a small example program of 13 lines, proving a temporal property required around 50 extra lines of annotations. However, some parts of the annotation process could be automated with tooling support but to achieve full automation is probably not possible. This is partly due to ranking functions that the framework requires which, in general, are not easy to generate automatically.

Formell verifikation är ett område inom teoretisk datalogi där man genom matematisk logik vill bevisa att ett program beter sig på ett visst sätt. Genom detta kan man bevisa att programmet följer en given specifikation och beter sig som man tänkt. Detta område kan delas upp i två separata delar. Den ena handlar om att visa hur programmet transformerar data och bygger på Hoare logik och deduktiv verifikation för att bevisa att programmet följer en viss specifikation. Den andra delen handlar om temporala egenskaper och använder sig av model checking och temporal logik. Dessa delar behandlas vanligtvis separat från varandra. Denna rapport bygger på ett logiskt system utvecklat av Alur och Chaudhuri [1] som används för att bevisa temporala egenskaper genom ett angreppssätt som använder Hoare-logik. Genom att använda detta system vill denna rapport undersöka huruvida det är möjligt att bevisa temporala egenskaper med hjälp av deduktiva verifierare och därigenom minska klyftan mellan dessa två områden av formel verifikation.

Rapporten finner att det är möjligt att använda Alur och Chaudhuri’s system för att bevisa temporala egenskaper genom deduktiva verifierare. I praktiska termer krävs det för mycket arbete för att kunna användas genom att manuellt skapa instruktioner till den deduktiva verifieraren. I ett litet exempelprogram på 13 rader kräves 50 extra rader av annotationer för att bevisa en viss temporal egenskap. Stora delar av den processen skulle dock kunna automatiseras med verktygsstöd. Att automatisera hela processen är dock antagligen inte möjligt. Detta är dels pågrund av att de rankning funktioner som systemet använder sig av är svåra att automatisera.