Boogie factors verification of Spec# programs into
- Generating the Intermediate Verification Language BoogiePL by encoding language semantics, using abstract interpretation and introducing ghost state.
- Verifying BoogiePL by generating Verification Conditions and proving them using “Simplify” (with plans of switch to “Zap”). This combination simplifies and separates the two tasks and allows use of abstract interpretation (good at calculating fixpoints) and theorem proving (good at handling quantification).
BoogiePL is a simple imperative language with fresh (unconstrained) variables, assume, assert, requires, ensures, function calls, heap and non-deterministic goto but no structured control.
A strength and a weakness is that functions calls are always verified by inserting the requires/ensures from the function spec not using the function definition itself. (The weakness is that this requires the creation of specs for every function.)
This builds on the authors’ previous work on ESC Modula3/Java. Simple loop invariants (especially those associated with object allocation/lifetime) are inferred to reduce need for trivial invariants.
The paper notes that separation of generation from proof is not always ideal because it leads to some duplication of reasoning support and it makes loop invariant generation harder.
Similar work is Caduceus and its IVL “Why”. Used by SMACK Hyper-V VCC and others.
Papers related to Boogie: A modular reusable verifier for object-oriented programs
- Verifying constant-time implementations [almeida:security:2016]
- Verifying Rust programs with SMACK [baranowski:atva:2018]
- Specification and verification: The Spec# experience [barnett:cacm:2011]
- The Boogie verification debugger [legoues:sefm:2011]
- Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
- Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]