Evolving and Extending Certificate Generation for a Program Verifier
Verification Condition (VC) generators play a critical role in automatic program verification. They reduce a program with a specification to a first-order logic formula (the VC), such that the validity of the VC implies the correctness of the input program. Such VC generators are core components of various automated program verifiers. Due to their wide use, it is essential that VC generators are correct, i.e., that the validity of the generated VC indeed implies the correctness of the input program. However, VC generators used in practice rarely have any formal correctness guarantees, which forces clients of VC generators to trust the entire generator code base.
Our prior work [1] addresses this issue by extending the Boogie VC generator [2] to produce a certificate, that is, a proof that can be checked by an independent tool. The Boogie VC generator applies a series of program-to-program transformations followed by a final program-to-VC transformation. On each run of the VC generator, the proof-producing Boogie generates a machine-checked proof in the Isabelle theorem prover for each transformation individually. The individual proofs are then combined to a single proof, which shows that the validity of the VC indeed implies the correctness of the input Boogie program.
While promising, the current implementation has two major limitations:
Outdated Codebase: The certification is based on an older version of Boogie and lives in a separate fork. Since then, Boogie has evolved significantly. Merging these changes into the proof-producing fork requires substantial adaptations to the certificate generation.
Limited Features Support: The Boogie VC generator is mainly used by automated program verifiers (such as external page Corral, external page Dafny, and Viper) that reduce the verification of a high-level program to the verification of a Boogie program, which is then given as an input to the Boogie VC generator. However, the current certification supports only a subset of Boogie features, which restricts its applicability. Many automated verifiers that rely on Boogie use additional features that are currently unsupported.
Project
This project aims to evolve and extend the Boogie certification to make it more maintainable and more broadly applicable. Specifically:
Redesign and Reimplement the Certification: Develop a lightweight approach to proof generation that minimizes changes to Boogie’s codebase. A key objective is to make the new implementation clean and maintainable enough to be potentially merged into the official Boogie repository. This opens up the opportunity for your work to become part of a widely used verification infrastructure, with direct impact on tools like Dafny and Viper.
Extend Feature Support: Add support for a broader set of Boogie features, with a focus on those required by major tools like Dafny and Viper. This involves understanding how Boogie translates these features during VC generation, identifying why these transformations are sound, and formally proving their correctness. A key part of the work is then designing and implementing mechanisms to automatically generate corresponding machine-checked proofs in Isabelle.
The planned steps of this project are:
Analyze and understand the change of the Boogie codebase since the certification fork.
Design a new architecture for the certificate generation that is decoupled from Boogie internals, improving maintainability.
Identify unsupported Boogie features required by tools like Dafny and Viper, and understand how their VC generation works.
Extend the proof-producing Boogie to support these features and thus verify the correctness of their VC generation.
Develop a test suite and evaluate the improved implementation.
Prerequisites
This project involves formal verification with the Isabelle theorem prover. Prior experience with interactive theorem provers (such as Isabelle, Coq or Lean) is highly valued, but is not strictly required. It is possible to learn to use Isabelle during the project given a strong background in formal methods (such as the background provided by the FMFP course).
References
[1] G. Parthasarathy, P. Müller, and A. J. Summers: Formally Validating a Practical Verification Condition Generator; Computer Aided Verification (CAV 2021)
[2] K. R. M. Leino: This is Boogie 2 (2008)