  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.
