|||Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 11-27. Springer, 2012. [ bib | .pdf ]|
Xavier Leroy, W. Appel, Andrew, Sandrine Blazy, and Gordon Stewart.
The CompCert Memory Model, Version 2.
Rapport de recherche RR-7987, INRIA, June 2012.
[ bib |
A memory model is an important component of the formal semantics of imperative programming languages: it specifies the behavior of operations over memory states, such as reads and writes. The formally verified CompCert C compiler uses a sophisticated memory model that is shared between the semantics of its source language (the CompCert subset of C) and intermediate languages. The algebraic properties of this memory model play an important role in the proofs of semantic preservation for the compiler. The initial design of the CompCert memory model is described in an article by Leroy and Blazy (J. Autom. Reasoning 2008). The present research report describes version 2 of this memory model, improving over the main limitations of version 1. The first improvement is to expose the byte-level, in-memory representation of integers and floats, while preserving desirable opaqueness properties of pointer values. The second improvement is the integration of a fine-grained mechanism of permissions (access rights), which supports more aggressive optimizations over read-only data, and paves the way towards shared-memory, data-race-free concurrency in the style of Appel's Verified Software Toolchain project.
Keywords: Memory models, formal semantics, verified compilation, CompCert
|||Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In 21st IEEE Symposium on Computer Arithmetic, pages 107-115. IEEE, 2013. [ bib | arXiv | .pdf ]|
Sandrine Blazy, Vincent Laporte, André Maronèze, and David Pichardie.
Formal verification of a C value analysis based on abstract
In Static analysis (SAS) .
[ bib |
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified C-compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool.
Alexis Fouilhé, David Monniaux, and Michaël Périn.
Efficient generation of correctness certificates for the abstract
domain of polyhedra.
In Static analysis (SAS) .
[ bib |
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations.
|||Static analysis (SAS), 2013. [ bib ]|
|||Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed data structures in Coq. In Interactive theorem proving (ITP), 2013. [ bib | arXiv ]|
This file was generated by bibtex2html 1.95.