An exercise in meta-verification with Why3.
This unpublished paper, co-authored with Maria João Frade, is dedicated to our colleague Luís Soares Barbosa, on the occasion of his 60th birthday.
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the question: “Who verifies the verifier?”.
We approach this meta-verification problem by considering a fundamental component of program verifiers: the “Verification Conditions Generator” (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. We derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language.
The workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove soundness and (an appropriate notion of) completeness of the logic w.r.t. the programming language semantics, then write a VCGen for the logic and prove its soundness. The VCGen is written as a program in WhyML (the internal Why3 programming language), that can be extracted to OCaml code. We reason about the (dynamic) program logic in Why3’s logic language, but then use the programming language to actually implement the VCGen.
The Why3 development is available on GitHub.