Verifying Temporal Properties Using Deductive Verifiers

Abstract: 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.