Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)

TL;DR

This paper demonstrates that the formal verification of Leroy and Blazy's memory model, originally done in Coq, can be largely automated using Why3, leading to a more efficient and almost-automatic proof process.

Contribution

The authors automated Leroy and Blazy's memory model proof in Why3, reducing manual effort and enabling extraction of a correct-by-construction concrete memory model.

Findings

Approximately one-third of verification conditions were automatically discharged by Why3.

The proof process was significantly streamlined with minimal manual intervention.

The approach allows for the extraction of a correct-by-construction concrete memory model.

Abstract

Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the challenge and automated their formalization using Why3, significantly reducing the proof effort. We systematically followed the Coq proofs and realized that in many cases at around one third of the way Why3 was able to discharge all VCs. Furthermore, the proofs still requiring interactions (e.g. induction, witnesses for existential proofs, assertions) were factorized isolating auxiliary results that we stated explicitly. In this way, we achieved an almost-automatic soundness and safety proof of the memory model. Nonetheless, our development allows an extraction of a correct-by-construction concrete memory model, going thus further than the preliminary Why version of Leroy and Blazy.