Sciweavers

Share
ICFP
2006
ACM

Modular development of certified program verifiers with a proof assistant

9 years 10 months ago
Modular development of certified program verifiers with a proof assistant
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. I take advantage of Coq's support for programming with dependent types and modules in the structure of my development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of ion into a verifier at a lower level. Using this library, it's possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product. Categories and Subject Descriptors F.3.1 [Specifying and Verifying and Reasoning about Programs]: Mechanical v...
Adam J. Chlipala
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2006
Where ICFP
Authors Adam J. Chlipala
Comments (0)
books