@inproceedings{Robert_Leroy_CPP2012,
author = {Valentin Robert and Xavier Leroy},
title = {A formally-verified alias analysis},
booktitle = {Certified Programs and Proofs (CPP 2012)},
pages = {11--27},
year = 2012,
volume = 7679,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pdf = {http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf}
}
@techreport{leroy:hal-00703441,
hal_id = {hal-00703441},
url = {http://hal.inria.fr/hal-00703441},
title = {{The CompCert Memory Model, Version 2}},
author = {Leroy, Xavier and Appel, Andrew, W. and Blazy, Sandrine and Stewart, Gordon},
abstract = {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},
language = {Anglais},
affiliation = {GALLIUM - INRIA Rocquencourt , Department of Computer Science , CELTIQUE - INRIA - IRISA},
pages = {26},
type = {Rapport de recherche},
institution = {INRIA},
number = {RR-7987},
year = {2012},
month = jun,
pdf = {http://hal.inria.fr/hal-00703441/PDF/RR-7987.pdf}
}
@inproceedings{Boldo_et_al_ARITH21,
author = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond },
title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
booktitle = {21st IEEE Symposium on Computer Arithmetic},
pages = {107--115},
year = 2013,
organization = {IEEE},
eprinttype = {HAL},
eprint = {hal-00743090/},
pdf = {http://hal.inria.fr/docs/00/78/09/03/PDF/article.pdf}
}
@inproceedings{Blazy_et_al_SAS2013,
author = {Sandrine Blazy and Vincent Laporte and André Maronèze and David Pichardie},
title = {Formal Verification of a {C} Value Analysis Based on Abstract Interpretation},
eprinttype = {HAL},
eprint = {hal-00812515},
abstract = {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.},
crossref = {SAS2013}
}
@inproceedings{Fouilhe_et_al_SAS2013,
author = {Alexis Fouilh\'e and David Monniaux and Micha\"el P\'erin},
title = {Efficient Generation of Correctness Certificates for
the Abstract Domain of Polyhedra},
eprinttype = {HAL},
eprint = {hal-00806990},
abstract = {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.},
crossref = {SAS2013}
}
@proceedings{SAS2013,
title = {Static analysis (SAS)},
booktitle = {Static analysis (SAS)},
year = 2013
}
@inproceedings{Braibant_Jourdan_Monniaux_ITP2013,
author = {Thomas Braibant and Jacques-Henri Jourdan and David Monniaux},
title = {Implementing hash-consed data structures in {C}oq},
booktitle = {Interactive theorem proving (ITP)},
eprinttype = {HAL},
eprint = {hal-00816672},
year = 2013
}
This file was generated by bibtex2html 1.95.