Units: 12 (6+6) or 24 (Honours)
Background:
Automatic software verifiers are fast and efficient for verifying simple programs–a user only needs to provide the specification and the verifier will complete the proof of correctness. However, they often struggle with real-world algorithms, which have complex properties and data types. Rather than abandon automatic verifiers, we are exploring ways to combine them with manual proof methods when needed, while retaining a high degree of automation. This is sometimes called cooperative verification.
This project will use Viper[1], a leading automatic software verifier, and Isabelle[2], an interactive proof assistant. We are currently developing methods to allow Viper to use proofs in Isabelle. We are particularly focused on graph algorithms, which are not handled well by automatic verifiers.
Project Goals/Options:
This project will demonstrate these cooperative methods through verification examples. This could involve:
- verifying graph algorithms in Viper, with some lemmas completed in Isabelle
- simplifying existing proofs in Viper by using simple lemmas in Isabelle
- building a library of graph functions in Viper, using properties already shown in Isabelle
Requirements:
Strong understanding of formal logic required (e.g. COMP1600 and/or COMP2620). Experience with Hoare Logic or other verification techniques will be very useful. COMP3610 or COMP4011 are helpful but not required.
References:
[1] https://www.pm.inf.ethz.ch/research/viper.html
[2] https://isabelle.in.tum.de/