@inproceedings{Blazy-Leroy-05, author = {Sandrine Blazy and Xavier Leroy}, title = {Formal verification of a memory model for {C}-like imperative languages}, booktitle = {International Conference on Formal Engineering Methods (ICFEM 2005)}, year = 2005, volume = 3785, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {280--299}, url = {http://xavierleroy.org/publi/memory-model.pdf}, urlpublisher = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11576280_20}, hal = {http://hal.inria.fr/inria-00077921/}, abstract = { This paper presents a formal verification with the Coq proof assistant of a memory model for C-like imperative languages. This model defines the memory layout and the operations that manage the memory. The model has been specified at two levels of abstraction and implemented as part of an ongoing certification in Coq of a moderately-optimising C compiler. Many properties of the memory have been verified in the specification. They facilitate the definition of precise formal semantics of C pointers. A certified OCaml code implementing the memory model has been automatically extracted from the specifications.}, xtopic = {compcert} }

@inproceedings{2006-Leroy-Bertot-Gregoire, author = {Yves Bertot and Benjamin Grégoire and Xavier Leroy}, title = {A structured approach to proving compiler optimizations based on dataflow analysis}, booktitle = {Types for Proofs and Programs, Workshop TYPES 2004}, year = 2006, volume = 3839, pages = {66-81}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, url = {http://xavierleroy.org/publi/proofs_dataflow_optimizations.pdf}, urlpublisher = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11617990_5}, hal = {http://hal.inria.fr/inria-00289549/}, abstract = { This paper reports on the correctness proof of compiler optimizations based on data-flow analysis. We formulate the optimizations and analyses as instances of a general framework for data-flow analyses and transformations, and prove that the optimizations preserve the behavior of the compiled programs. This development is a part of a larger effort of certifying an optimizing compiler by proving semantic equivalence between source and compiled code.} }

@inproceedings{2006-Leroy-compcert, author = {Xavier Leroy}, title = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant}, booktitle = {33rd ACM symposium on Principles of Programming Languages}, year = 2006, publisher = {ACM Press}, pages = {42--54}, url = {http://xavierleroy.org/publi/compiler-certif.pdf}, urlpublisher = {http://doi.acm.org/10.1145/1111037.1111042}, hal = {http://hal.inria.fr/inria-00000963/}, abstract = {This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.}, pubkind = {conf-int-mono} }

@inproceedings{2006-Leroy-coindsem, author = {Xavier Leroy}, title = {Coinductive big-step operational semantics}, booktitle = {European Symposium on Programming (ESOP'06)}, year = 2006, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 3924, pages = {54-68}, url = {http://xavierleroy.org/publi/coindsem.pdf}, urlpublisher = {http://dx.doi.org/10.1007/11693024_5}, hal = {http://hal.inria.fr/inria-00289545/}, abstract = {This paper illustrates the use of co-inductive definitions and proofs in big-step operational semantics, enabling the latter to describe diverging evaluations in addition to terminating evaluations. We show applications to proofs of type soundness and to proofs of semantic preservation for compilers. (See \verb|http://gallium.inria.fr/~xleroy/publi/coindsem/| for the Coq on-machine formalization of these results.)}, pubkind = {conf-int-mono} }

@inproceedings{2006-Leroy-Blazy-Dargaye, author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy}, title = {Formal Verification of a {C} Compiler Front-End}, booktitle = {FM 2006: Int. Symp. on Formal Methods}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = 4085, year = 2006, pages = {460--475}, url = {http://xavierleroy.org/publi/cfront.pdf}, urlpublisher = {http://dx.doi.org/10.1007/11813040_31}, hal = {http://hal.inria.fr/inria-00106401/}, abstract = {This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.}, pubkind = {conf-int-multi} }

@techreport{2006-Leroy-Appel-listmachine-tr, author = {Appel, Andrew W. and Leroy, Xavier}, title = {A list-machine benchmark for mechanized metatheory}, year = {2006}, institution = {INRIA}, number = {5914}, type = {Research report}, hal = {http://hal.inria.fr/inria-00077531/}, abstract = {We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be done without binders or alpha-conversion. We propose specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.} }

@inproceedings{2007-Blazy-Appel-Cminor-sos, author = {Andrew W. Appel and Sandrine Blazy}, title = {Separation logic for small-step {Cminor}}, booktitle = {Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 4732, pages = {5--21}, year = 2007, mon = sep, url = {http://www.ensiie.fr/~blazy/AppelBlazy07.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-540-74591-4_3}, hal = {http://hal.inria.fr/inria-00165915/}, pubkind = {conf-int-mono} }

@inproceedings{2007-Blazy-C-semantics, author = {Sandrine Blazy}, title = {Experiments in validating formal semantics for {C}}, booktitle = {Proceedings of the C/C++ Verification Workshop}, pages = {95--102}, year = 2007, mon = jul, url = {http://www.ensiie.fr/~blazy/C07Blazy.pdf}, hal = {http://hal.inria.fr/inria-00292043/}, publisher = {Technical report ICIS-R07015, Radboud University Nijmegen}, pubkind = {conf-int-mono} }

@inproceedings{2007-Dargaye-JFLA, author = {Zaynah Dargaye}, title = {Décurryfication certifiée}, booktitle = {Journées Francophones des Langages Applicatifs (JFLA'07)}, pages = {119--134}, publisher = {INRIA}, year = {2007}, url = {http://gallium.inria.fr/~dargaye/publications/certdec.pdf}, hal = {http://hal.inria.fr/inria-00338974/}, pubkind = {conf-fr-mono} }

@inproceedings{2007-Dargaye-Leroy-LPAR, author = {Zaynah Dargaye and Xavier Leroy}, title = {Mechanized verification of {CPS} transformations}, booktitle = {Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007}, year = 2007, series = {Lecture Notes in Artificial Intelligence}, volume = 4790, publisher = {Springer}, pages = {211--225}, url = {http://xavierleroy.org/publi/cps-dargaye-leroy.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-540-75560-9_17}, hal = {http://hal.inria.fr/inria-00289541/}, abstract = { Transformation to continuation-passing style (CPS) is often performed by optimizing compilers for functional programming languages. As part of the development and proof of correctness of a compiler for the mini-ML functional language, we have mechanically verified the correctness of two CPS transformations for a call-by-value $\lambda$-calculus with $n$-ary functions, recursive functions, data types and pattern-matching. The transformations generalize Plotkin's original call-by-value transformation and Danvy and Nielsen's optimized transformation, respectively. We used the Coq proof assistant to formalize the transformations and conduct and check the proofs. Originalities of this work include the use of big-step operational semantics to avoid difficulties with administrative redexes, and of two-sorted de Bruijn indices to avoid difficulties with $\alpha$-conversion.}, pubkind = {conf-int-mono} }

@inproceedings{2007-Doligez-Bonichon-Delahaye, author = {Richard Bonichon and David Delahaye and Damien Doligez}, title = {{Zenon}: an Extensible Automated Theorem Prover Producing Checkable Proofs}, booktitle = {Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007}, year = 2007, series = {Lecture Notes in Artificial Intelligence}, volume = 4790, publisher = {Springer}, pages = {151--165}, url = {http://focal.inria.fr/zenon/zenlpar07.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-540-75560-9_13}, hal = {http://hal.inria.fr/inria-00315920/}, abstract = { We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.}, pubkind = {conf-int-multi} }

@inproceedings{2007-Leroy-Appel-listmachine-lfmtp, author = {Appel, Andrew W. and Leroy, Xavier}, title = {A list-machine benchmark for mechanized metatheory (extended abstract)}, booktitle = {Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP'06)}, year = {2007}, series = {Electronic Notes in Computer Science}, volume = {174/5}, pages = {95--108}, url = {http://xavierleroy.org/publi/listmachine-lfmtp.pdf}, urlpublisher = {http://dx.doi.org/10.1016/j.entcs.2007.01.020}, hal = {http://hal.inria.fr/inria-00289543/}, abstract = {Short version of \cite{2006-Leroy-Appel-listmachine-tr}.}, pubkind = {conf-int-mono} }

@article{2007-Leroy-Grall, author = {Xavier Leroy and Hervé Grall}, title = {Coinductive big-step operational semantics}, journal = {Information and Computation}, volume = 207, number = 2, pages = {284--304}, year = 2009, url = {http://xavierleroy.org/publi/coindsem-journal.pdf}, urlpublisher = {http://dx.doi.org/10.1016/j.ic.2007.12.004}, hal = {http://hal.inria.fr/inria-00309010/}, abstract = {Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.}, pubkind = {journal-int-mono} }

@article{2007-Blazy-C-chronique, author = {Sandrine Blazy}, title = {Comment gagner confiance en {C} ?}, journal = {Technique et Science Informatiques}, year = {2007}, volume = {26}, number = {9}, pages = {1195-1200}, url = {http://www.ensiie.fr/~blazy/TSI07Blazy.pdf}, hal = {http://hal.inria.fr/inria-00292049/}, pubkind = {journal-fr-mono} }

@inproceedings{2007-Blazy-JGA, author = {Sandrine Blazy and Benoît Robillard and Eric Soutif}, title = {Coloration avec préférences dans les graphes triangulés}, booktitle = {Journées Graphes et Algorithmes (JGA'07)}, year = {2007}, month = nov, url = {http://www.liafa.jussieu.fr/jga07/JGA07.pdf}, pubkind = {conf-fr-mono} }

@techreport{2007-Blazy-Appel-Cminor-sosRR, author = {Andrew W. Appel and Sandrine Blazy}, title = {Separation logic for small-step {Cminor} (extended version)}, note = {29 pages}, year = 2007, mon = mar, institution = {INRIA}, number = {6138}, type = {Research report}, hal = {http://hal.inria.fr/inria-00134699/} }

@article{2008-Leroy-Blazy-memory-model, author = {Xavier Leroy and Sandrine Blazy}, title = {Formal verification of a {C}-like memory model and its uses for verifying program transformations}, journal = {Journal of Automated Reasoning}, volume = 41, number = 1, pages = {1--31}, url = {http://xavierleroy.org/publi/memory-model-journal.pdf}, urlpublisher = {http://dx.doi.org/10.1007/s10817-008-9099-0}, hal = {http://hal.inria.fr/inria-00289542/}, year = 2008, pubkind = {journal-int-multi} }

@article{2008-Leroy-Rideau-Serpette-pmov, author = {Laurence Rideau and Bernard Paul Serpette and Xavier Leroy}, title = {Tilting at windmills with {Coq}: Formal verification of a compilation algorithm for parallel moves}, journal = {Journal of Automated Reasoning}, volume = 40, number = 4, pages = {307--326}, url = {http://xavierleroy.org/publi/parallel-move.pdf}, urlpublisher = {http://dx.doi.org/10.1007/s10817-007-9096-8}, hal = {http://hal.inria.fr/inria-00289709/}, year = 2008, pubkind = {journal-int-multi} }

@inproceedings{2008-Tristan-Leroy-POPL, author = {Jean-Baptiste Tristan and Xavier Leroy}, title = {Formal verification of translation validators: A case study on instruction scheduling optimizations}, booktitle = {Proceedings of the 35th {ACM} Symposium on Principles of Programming Languages (POPL'08)}, pages = {17--27}, publisher = {ACM Press}, year = 2008, month = jan, url = {http://xavierleroy.org/publi/validation-scheduling.pdf}, hal = {http://hal.inria.fr/inria-00289540/}, urlpublisher = {http://doi.acm.org/10.1145/1328897.1328444}, pubkind = {conf-int-mono}, abstract = {Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of its semantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The validators are designed for two instruction scheduling optimizations: list scheduling and trace scheduling.} }

@inproceedings{2008-Blazy-JFLA, author = {Sandrine Blazy and Benoît Robillard and Eric Soutif}, title = {Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes}, booktitle = {Journées Francophones des Langages Applicatifs (JFLA'08)}, year = 2008, address = {Étretat, France}, month = jan, pages = {31--46}, url = {http://www.ensiie.fr/~blazy/JFLABRS08.pdf}, hal = {http://hal.inria.fr/inria-00202713/}, pubkind = {conf-fr-mono} }

@techreport{2007-Bertot-progsem-tr, author = {Yves Bertot}, title = {Theorem proving support in programming language semantics}, year = {2007}, institution = {INRIA}, type = {Research report}, number = {6242}, hal = {http://hal.inria.fr/inria-00160309/} }

@incollection{2009-Bertot-progsem, author = {Yves Bertot}, title = {Theorem proving support in programming language semantics}, booktitle = {From Semantics to Computer Science -- Essays in Honour of {Gilles} {Kahn}}, editor = {Y. Bertot and G. Huet and J.-J. Lévy and G. Plotkin}, publisher = {Cambridge University Press}, pages = {337-362}, year = {2009}, urlpublisher = {http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521518253} }

@unpublished{2006-Bertot-Tarski, title = {Extending the Calculus of Constructions with {Tarski}'s fix-point theorem}, author = {Yves Bertot}, abstract = {We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tool to potentially non-terminating functions. This is only possible if we extend the logical framework by adding the axioms that correspond to classical logic. We claim that the extended framework makes it possible to reason about terminating and non-terminating computations and we show that common facilities of the calculus of inductive construction, like program extraction can be extended to also handle the new functions.}, year = {2006}, hal = {http://hal.inria.fr/inria-00105529/} }

@inproceedings{2008-Bertot-Komendantsky, title = {Fixed point semantics and partial recursion in {Coq}}, author = {Yves Bertot and Vladimir Komendantsky}, booktitle = {10th int. ACM SIGPLAN conference on Principles and Practice of Declarative Programming (PPDP 2008)}, publisher = {ACM Press}, year = 2008, pages = {89-96}, abstract = {We propose to use the least fixed point theorem as a basis to define recursive functions in the Calculus of Inductive Constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tools to potentially non-terminating functions. This is only possible if we extend the logical framework by adding some axioms of classical logic. We claim that the extended framework makes it possible to reason about terminating or non-terminating computations and we show that extraction can also be extended to handle the new functions.}, hal = {http://hal.inria.fr/inria-00190975/}, urlpublisher = {http://doi.acm.org/10.1145/1389449.1389461}, pubkind = {conf-int-mono} }

@inproceedings{2008-Blazy-ROADEF, author = {Sandrine Blazy and Benoît Robillard and Éric Soutif}, title = {Coloration avec préférences: complexité, inégalités valides et vérification formelle}, booktitle = {ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision}, year = {2008}, hal = {http://hal.inria.fr/inria-00260712/}, pubkind = {conf-fr-mono} }

@article{Leroy-backend, author = {Xavier Leroy}, title = {A formally verified compiler back-end}, journal = {Journal of Automated Reasoning}, volume = 43, number = 4, pages = {363--446}, year = 2009, url = {http://xavierleroy.org/publi/compcert-backend.pdf}, urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4}, hal = {http://hal.inria.fr/inria-00360768/}, pubkind = {journal-int-mono} }

@article{Blazy-Leroy-Clight-09, author = {Sandrine Blazy and Xavier Leroy}, title = {Mechanized semantics for the {Clight} subset of the {C} language}, year = 2009, journal = {Journal of Automated Reasoning}, url = {http://xavierleroy.org/publi/Clight.pdf}, hal = {http://hal.inria.fr/inria-00352524/}, urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3}, volume = 43, number = 3, pages = {263-288} }

@inproceedings{Tristan-Leroy-LCM, author = {Jean-Baptiste Tristan and Xavier Leroy}, title = {Verified Validation of {Lazy} {Code} {Motion}}, booktitle = {Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09)}, year = 2009, pages = {316--326}, url = {http://xavierleroy.org/publi/validation-LCM.pdf}, urlpublisher = {http://doi.acm.org/10.1145/1542476.1542512}, hal = {http://hal.archives-ouvertes.fr/inria-00415865/}, pubkind = {conf-int-mono} }

@inproceedings{Blazy-Robillard-splitting, author = {Sandrine Blazy and Benoît Robillard}, title = {Live-range Unsplitting for Faster Optimal Coalescing}, booktitle = {Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009)}, pages = {70--79}, publisher = {ACM Press}, year = 2009, url = {http://www.ensiie.fr/~blazy/LCTES09.pdf}, urlpublisher = {http://doi.acm.org/10.1145/1542452.1542462}, hal = {http://hal.inria.fr/inria-00387749/}, pubkind = {conf-int-mono} }

@inproceedings{Letouzey-CiE-08, author = {Letouzey, Pierre}, booktitle = {Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008}, title = {Extraction in {Coq}: An Overview}, pages = {359--369}, year = 2008, urlpublisher = {http://dx.doi.org/10.1007/978-3-540-69407-6_39}, hal = {http://hal.archives-ouvertes.fr/hal-00338973/}, volume = 5028, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pubkind = {conf-int-mono} }

@incollection{Bertot-absint-08, author = {Yves Bertot}, title = {Structural abstract interpretation: A formal study using {Coq}}, booktitle = {Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008}, editor = {Ana Bove and Jorge Sousa Pinto}, series = {Lecture Notes in Computer Science}, volume = 5520, publisher = {Springer}, year = 2009, pages = {153-194}, urlpublisher = {http://dx.doi.org/10.1007/978-3-642-03153-3_4}, hal = {http://hal.inria.fr/inria-00329572/} }

@phdthesis{Blazy-HDR, author = {Sandrine Blazy}, title = {Sémantiques formelles}, type = {Habilitation à diriger les recherches}, school = {Université Évry Val d'Essone}, year = 2008, month = oct, url = {http://www.ensiie.fr/~blazy/hdr.html}, hal = {http://tel.archives-ouvertes.fr/tel-00336576/} }

@inproceedings{Glondu-JFLA09, author = {Stéphane Glondu}, title = {Extraction certifiée dans {Coq}-en-{Coq}}, booktitle = {Journées Francophones des Langages Applicatifs (JFLA'09)}, publisher = {INRIA}, year = {2009}, pages = {105--118}, url = {http://stephane.glondu.net/jfla09.pdf}, hal = {http://hal.inria.fr/inria-00362717/}, pubkind = {conf-fr-mono} }

@article{Dargaye-Leroy-uncurrying, author = {Zaynah Dargaye and Xavier Leroy}, title = {A verified framework for higher-order uncurrying optimizations}, journal = {Higher-Order and Symbolic Computation}, url = {http://xavierleroy.org/publi/higher-order-uncurrying.pdf}, urlpublisher = {http://dx.doi.org/10.1007/s10990-010-9050-z}, year = 2009, volume = 22, number = 3, pages = {199--231} }

@article{Leroy-Compcert-CACM, author = {Xavier Leroy}, title = {Formal verification of a realistic compiler}, journal = {Communications of the ACM}, year = 2009, volume = 52, number = 7, pages = {107--115}, url = {http://xavierleroy.org/publi/compcert-CACM.pdf}, urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814}, hal = {http://hal.archives-ouvertes.fr/inria-00415861/}, pubkind = {journal-int-mono}, abstract = {This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.} }

@inproceedings{Tristan-Leroy-softpipe, author = {Jean-Baptiste Tristan and Xavier Leroy}, title = {A simple, verified validator for software pipelining}, booktitle = {Proceedings of the 37th {ACM} Symposium on Principles of Programming Languages (POPL'10)}, pages = {83--92}, publisher = {ACM Press}, year = 2010, url = {http://xavierleroy.org/publi/validation-softpipe.pdf}, urlpublisher = {http://doi.acm.org/10.1145/1706299.1706311} }

@phdthesis{Dargaye-these, author = {Zaynah Dargaye}, title = {Vérification formelle d'un compilateur pour langages fonctionnels}, school = {Université Paris 7 Diderot}, year = 2009, month = jul, hal = {http://tel.archives-ouvertes.fr/tel-00452440/} }

@phdthesis{Tristan-these, author = {Jean-Baptise Tristan}, title = {Formal verification of translation validators}, school = {Université Paris 7 Diderot}, month = nov, year = 2009, hal = {http://tel.archives-ouvertes.fr/tel-00437582/} }

@article{Leroy-La-Recherche-10, author = {Xavier Leroy}, title = {Comment faire confiance à un compilateur?}, journal = {La Recherche}, note = {Les cahiers de l'INRIA}, year = {2010}, month = apr, volume = 440, url = {http://xavierleroy.org/publi/cahiers-inria-2010.pdf}, urlpublisher = {http://www.lescahiersinria.fr/sites/default/files/inria-n440-avril10.pdf}, xtopic = {compcert}, popularscience = {yes}, abstract = {(In French.) A short introduction to compiler verification, published in the French popular science magazine La Recherche.} }

@inproceedings{Rideau-Leroy-regalloc, author = {Silvain Rideau and Xavier Leroy}, title = {Validating register allocation and spilling}, booktitle = {Compiler Construction (CC 2010)}, year = 2010, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 6011, pages = {224-243}, xtopic = {compcert}, url = {http://xavierleroy.org/publi/validation-regalloc.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-642-11970-5_13}, abstract = {Following the translation validation approach to high-assurance compilation, we describe a new algorithm for validating {\em a posteriori} the results of a run of register allocation. The algorithm is based on backward dataflow inference of equations between variables, registers and stack locations, and can cope with sophisticated forms of spilling and live range splitting, as well as many forms of architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.} }

@incollection{Leroy-Marktoberdorf-09, author = {Xavier Leroy}, title = {Mechanized semantics}, booktitle = {Logics and languages for reliability and security}, editors = {J. Esparza and B. Spanfelner and O. Grumberg}, series = {NATO Science for Peace and Security Series D: Information and Communication Security}, volume = 25, pages = {195--224}, publisher = {IOS Press}, year = {2010}, url = {http://xavierleroy.org/courses/Marktoberdorf-2009/notes.pdf}, urlpublisher = {http://dx.doi.org/10.3233/978-1-60750-100-8-195}, xtopic = {mechsem}, abstract = {The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and over generic program transformations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimination) and its proof of correctness.} }

@inproceedings{Leroy-PPES-2011, author = {Ricardo {Bedin França} and Denis Favre-Felix and Xavier Leroy and Marc Pantel and Jean Souyris}, title = {Towards Optimizing Certified Compilation in Flight Control Software}, booktitle = {Workshop on Predictability and Performance in Embedded Systems (PPES 2011)}, pages = {59--68}, series = {OpenAccess Series in Informatics}, volume = 18, publisher = {Dagstuhl Publishing}, year = {2011}, url = {http://hal.archives-ouvertes.fr/inria-00551370/}, urlpublisher = {http://dx.doi.org/10.4230/OASIcs.PPES.2011.59}, xtopic = {compcert}, abstract = { This work presents a preliminary evaluation of the use of the CompCert formally specified and verified optimizing compiler for the development of level A critical flight control software. First, the motivation for choosing CompCert is presented, as well as the requirements and constraints for safety-critical avionics software. The main point is to allow optimized code generation by relying on the formal proof of correctness instead of the current un-optimized generation required to produce assembly code structurally similar to the algorithmic language (and even the initial models) source code. The evaluation of its performance (measured using WCET) is presented and the results are compared to those obtained with the currently used compiler. Finally, the paper discusses verification and certification issues that are raised when one seeks to use CompCert for the development of such critical software. } }

@inproceedings{Leroy-POPL11, author = {Xavier Leroy}, title = {Verified squared: does critical software deserve verified tools?}, booktitle = {38th symposium Principles of Programming Languages}, pages = {1--2}, year = 2011, publisher = {ACM Press}, note = {Abstract of invited lecture}, url = {http://xavierleroy.org/publi/popl11-invited-talk.pdf}, urlpublisher = {http://dx.doi.org/10.1145/1926385.1926387}, xtopic = {compcert}, abstract = { The formal verification of programs have progressed tremendously in the last decade. Principled but once academic approaches such as Hoare logic and abstract interpretation finally gave birth to quality verification tools, operating over source code (and not just idealized models thereof) and able to verify complex real-world applications. In this talk, I review some of the obstacles that remain to be lifted before source-level verification tools can be taken really seriously in the critical software industry: not just as sophisticated bug-finders, but as elements of absolute confidence in the correctness of a critical application. } }

@inproceedings{Bedin-Franca-ERTS-2012, author = {Ricardo {Bedin França} and Sandrine Blazy and Denis Favre-Felix and Xavier Leroy and Marc Pantel and Jean Souyris}, title = {Formally verified optimizing compilation in {ACG}-based flight control software}, booktitle = {Embedded Real Time Software and Systems (ERTS 2012)}, year = 2012, url = {http://hal.inria.fr/hal-00653367/}, xtopic = {compcert}, abstract = {This work presents an evaluation of the CompCert formally specified and verified optimizing compiler for the development of DO-178 level A flight control software. First, some fundamental characteristics of flight control software are presented and the case study program is described. Then, the use of CompCert is justified: its main point is to allow optimized code generation by relying on the formal proof of correctness and additional compilation information instead of the current un-optimized generation required to produce predictable assembly code patterns. The evaluation of its performance (measured using WCET and code size) is presented and the results are compared to those obtained with the currently used compiler.} }

@inproceedings{Jourdan-Pottier-Leroy, author = {Jacques-Henri Jourdan and François Pottier and Xavier Leroy}, title = {Validating {LR(1)} Parsers}, booktitle = {Programming Languages and Systems -- 21st European Symposium on Programming, ESOP 2012}, url = {http://xavierleroy.org/publi/validated-parser.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-642-28869-2_20}, year = 2012, pages = {397--416}, series = {Lecture Notes in Computer Science}, volume = 7211, publisher = {Springer}, xtopic = {compcert}, abstract = { An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. This validation of the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.} }

@inproceedings{Leroy-APLAS-2012, author = {Xavier Leroy}, title = {Mechanized Semantics for Compiler Verification}, note = {Abstract of invited talk}, booktitle = {Programming Languages and Systems, 10th Asian Symposium, APLAS 2012}, editor = {Ranjit Jhala and Atsushi Igarashi}, year = {2012}, pages = {386--388}, series = {Lecture Notes in Computer Science}, volume = 7705, publisher = {Springer}, url = {http://xavierleroy.org/publi/mechanized-semantics-aplas-cpp-2012.pdf}, urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35182-2_27}, xtopic = {mechsem}, refereed = {no}, abstract = {The formal verification of compilers and related programming tools depends crucially on the availability of appropriate mechanized semantics for the source, intermediate and target languages. In this invited talk, I review various forms of operational semantics and their mechanization, based on my experience with the formal verification of the CompCert~C compiler.} }

@inproceedings{Robert-Leroy-2012, author = {Valentin Robert and Xavier Leroy}, title = {A Formally-Verified Alias Analysis}, booktitle = {Certified Programs and Proofs (CPP 2012)}, year = 2012, series = {Lecture Notes in Computer Science}, volume = 7679, pages = {11-26}, publisher = {Springer}, urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35308-6_5}, url = {http://xavierleroy.org/publi/alias-analysis.pdf}, xtopic = {compcert}, abstract = {This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is intraprocedural, flow-sensitive, field-sensitive, and untyped. Its soundness proof follows the general style of abstract interpretation. The analysis is designed to fit in the CompCert C verified compiler, supporting future aggressive optimizations over memory accesses.} }

@techreport{Leroy-Appel-Blazy-Stewart-memory-v2, author = {Xavier Leroy and Andrew W. Appel and Sandrine Blazy and Gordon Stewart}, title = {The {CompCert} Memory Model, Version 2}, institution = {INRIA}, type = {Research report}, number = {RR-7987}, year = {2012}, month = jun, url = {http://hal.inria.fr/hal-00703441}, xtopic = {compcert}, 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.} }

@inproceedings{Boldo-Jourdan-Leroy-Melquiond-2013, title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic}, author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume}, booktitle = {ARITH, 21st IEEE International Symposium on Computer Arithmetic}, pages = {107-115}, publisher = {IEEE Computer Society Press}, url = {http://hal.inria.fr/hal-00743090}, year = 2013, xtopic = {compcert}, abstract = {Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, this is not sufficient to guarantee the final result of a program, as several other actors are involved: programming language, compiler, architecture. The CompCert formally-verified compiler provides a solution to this problem: this compiler comes with a mathematical specification of the semantics of its source language (a large subset of ISO C90) and target platforms (ARM, PowerPC, x86-SSE2), and with a proof that compilation preserves semantics. In this paper, we report on our recent success in formally specifying and proving correct CompCert's compilation of floating-point arithmetic. Since CompCert is verified using the Coq proof assistant, this effort required a suitable Coq formalization of the IEEE-754 standard; we extended the Flocq library for this purpose. As a result, we obtain the first formally verified compiler that provably preserves the semantics of floating-point programs.} }

@incollection{Leroy-Appel-Blazy-Stewart-memory, author = {Leroy, Xavier and Appel, Andrew W. and Blazy, Sandrine and Stewart, Gordon}, title = {The {CompCert} memory model}, year = {2014}, month = apr, booktitle = {Program Logics for Certified Compilers}, editor = {Appel, Andrew W.}, publisher = {Cambridge University Press}, url = {http://vst.cs.princeton.edu/} }

@article{Boldo-Jourdan-Leroy-Melquiond-JAR, title = {Verified Compilation of Floating-Point Computations}, author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume}, journal = {Journal of Automated Reasoning}, year = 2015, volume = 54, number = 2, pages = {135--163}, xtopic = {compcert}, url = {http://xavierleroy.org/publi/floating-point-compcert.pdf}, urlpublisher = {http://dx.doi.org/10.1007/s10817-014-9317-x}, abstract = {Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, this is not sufficient to guarantee the final result of a program, as several other actors are involved: programming language, compiler, and architecture. The CompCert formally-verified compiler provides a solution to this problem: this compiler comes with a mathematical specification of the semantics of its source language (a large subset of ISO C99) and target platforms (ARM, PowerPC, x86-SSE2), and with a proof that compilation preserves semantics. In this paper, we report on our recent success in formally specifying and proving correct CompCert's compilation of floating-point arithmetic. Since CompCert is verified using the Coq proof assistant, this effort required a suitable Coq formalization of the IEEE-754 standard; we extended the Flocq library for this purpose. As a result, we obtain the first formally verified compiler that provably preserves the semantics of floating-point programs.} }

@inproceedings{Kastner-LBSSF-2017, title = {Closing the gap -- The formally verified optimizing compiler {CompCert}}, author = {K{\"a}stner, Daniel and Leroy, Xavier and Blazy, Sandrine and Schommer, Bernhard and Schmidt, Michael and Ferdinand, Christian}, urllocal = {http://xavierleroy.org/publi/compcert-SSS2017.pdf}, hal = {https://hal.inria.fr/hal-01399482}, urlpublisher = {http://scsc.org.uk/p135}, booktitle = {SSS'17: Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium}, year = {2017}, publisher = {CreateSpace}, pages = {163--180}, xtopic = {compcert}, abstract = {CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be free from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. CompCert's intended use is the compilation of safety-critical and mission-critical software meeting high levels of assurance. This article gives an overview of the design of CompCert and its proof concept, summarizes the resulting confidence argument, and gives an overview of relevant tool qualification strategies. We briefly summarize practical experience and give an overview of recent CompCert developments.} }

@inproceedings{Leroy-BKSPF-2016, author = {Xavier Leroy and Sandrine Blazy and Daniel K\"astner and Bernhard Schommer and Markus Pister and Christian Ferdinand}, title = {CompCert -- A Formally Verified Optimizing Compiler}, booktitle = {ERTS 2016: Embedded Real Time Software and Systems}, publisher = {SEE}, year = 2016, url = {http://xavierleroy.org/publi/erts2016_compcert.pdf}, hal = {https://hal.inria.fr/hal-01238879}, xtopic = {compcert}, abstract = {CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from mis-compilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the design of CompCert and its proof concept and then focuses on aspects relevant for industrial application. We briefly summarize practical experience and give an overview of recent CompCert development aiming at industrial usage. CompCert’s intended use is the compilation of life-critical and mission-critical software meeting high levels of assurance. In this context tool qualification is of paramount importance. We summarize the confidence argument of CompCert and give an overview of relevant qualification strategies.} }

@inproceedings{Jourdan-LBLP-2015, author = {Jacques-Henri Jourdan and Vincent Laporte and Sandrine Blazy and Xavier Leroy and David Pichardie}, title = {A Formally-Verified {C} Static Analyzer}, booktitle = {POPL 2015: 42nd symposium Principles of Programming Languages}, publisher = {ACM Press}, year = 2015, url = {http://xavierleroy.org/publi/verasco-popl2015.pdf}, urlpublisher = {http://dx.doi.org/10.1145/2676726.2676966}, pages = {247-259}, xtopic = {analysis}, abstract = {This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO~C~1999 language (excluding recursion and dynamic allocation). Verasco establishes the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified C~compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.} }

@phdthesis{jourdan:tel-01327023, title = {{Verasco: a Formally Verified C Static Analyzer}}, author = {Jourdan, Jacques-Henri}, hal = {https://hal.archives-ouvertes.fr/tel-01327023}, school = {{Universit\'e Paris 7 Diderot}}, year = {2016}, month = may, type = {PhD thesis}, hal_id = {tel-01327023}, hal_version = {v1} }

@inproceedings{Bourke-BDLPR-2017, title = {A formally verified compiler for {Lustre}}, author = {Timothy Bourke and Lélio Brun and Pierre-Évariste Dagand and Xavier Leroy and Marc Pouzet and Lionel Rieg}, booktitle = {PLDI 2017: Programming Language Design and Implementation}, pages = {586-601}, publisher = {ACM Press}, year = 2017, url = {http://xavierleroy.org/publi/velus-pldi17.pdf}, hal = {https://hal.inria.fr/hal-01512286/}, urlpublisher = {https://doi.org/10.1145/3062341.3062358}, xtopic = {compcert}, abstract = {The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs. We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.} }

@inproceedings{CompCert-ERTS-2018, author = {Daniel Kästner and Ulrich Wünsche and Jörg Barrho and Marc Schlickling and Bernhard Schommer and Michael Schmidt and Christian Ferdinand and Xavier Leroy and Sandrine Blazy}, title = {{CompCert}: Practical experience on integrating and qualifying a formally verified optimizing compiler}, booktitle = {ERTS 2018: Embedded Real Time Software and Systems}, publisher = {SEE}, year = 2018, month = jan, hal = {https://hal.inria.fr/hal-01643290}, url = {http://xavierleroy.org/publi/erts2018_compcert.pdf}, xtopic = {compcert}, abstract = {CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from mis-compilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the use of CompCert to gain certification credits for a highly safety-critical industry application, certified according to IEC 60880. We will briefly introduce the target application, illustrate the process of changing the existing compiler infrastructure to CompCert, and discuss performance characteristics. The main part focuses on the tool qualification strategy, in particular on how to take advantage of the formal correctness proof in the certification process.} }

@inproceedings{AIS-annot-WCET-2018, title = {Embedded Program Annotations for {WCET} Analysis}, author = {Schommer, Bernhard and Cullmann, Christoph and Gebhard, Gernot and Leroy, Xavier and Schmidt, Michael and Wegener, Simon}, hal = {https://hal.inria.fr/hal-01848686}, booktitle = {WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis}, publisher = {Dagstuhl Publishing}, series = {OASIcs}, volume = 63, year = {2018}, month = jul, urlpublisher = {http://dx.doi.org/10.4230/OASIcs.WCET.2018.8}, doi = {10.4230/OASIcs.WCET.2018.8}, abstract = {We present \verb'__builtin_ais_annot()', a user-friendly, versatile way to transfer annotations (also known as flow facts) written on the source code level to the machine code level. To do so, we couple two tools often used during the development of safety-critical hard real-time systems, the formally verified C compiler CompCert and the static WCET analyzer aiT. CompCert stores the AIS annotations given via \verb'__builtin_ais_annot()' in a special section of the ELF binary, which can later be extracted automatically by aiT.} }

*This file was generated by
bibtex2html 1.98.*