Publications of Sandrine Blazy

Load the BibTeX file

Books

  1. Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Sandrine Blazy, Christine Paulin-Mohring, David PichardieS. Blazy, C. Paulin-Mohring, D. Pichardie (eds.), Lecture Notes in Computer Science, Springer, 2013. download

Academic Journals

  1. Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009.

Book Chapters

  1. Xavier Leroy, W, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert memory model. In Program Logics for Certified Compilers, Andrew W. Appel (ed.), Cambridge University Press, December 2013. download

International Conferences

  1. Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In SAS - 20th Static Analysis Symposium, Manuel Fahndrich, Francesco Logozzo (eds.), Volume Lecture Notes in Computer Science, Pages 324-344, Seattle, United States, 2013. download
  2. Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In VSTTE - Verified Software: Theories, Tools and Experiments, Ernie Cohen, Andrey Rybalchenko (eds.), Lecture Notes in Computer Science, Volume 8164, Pages 281-303, Menlo Park, United States, 2013. download
  3. Jael Kriener, Andy King, Sandrine Blazy. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq. In 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Tom Schrijvers (ed.), Pages 37-48, Madrid, Spain, September 2013. download
  4. Ricardo Bedin Franca, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In ERTS2 congress, to appear, 2012.
  5. Ricardo Bedin Frana, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In ERTS2 2012: Embedded Real Time Software and Systems, Toulouse, France, February 2012. download
  6. Sandrine Blazy, Benot Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. In 19th European Symposium on Programming (ESOP), Volume 6012, Pages 145-164, Chypre Paphos, March 2010.
  7. Sandrine Blazy, Benot Robillard. Live-range Unsplitting for Faster Optimal Coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), Pages 70-79, 2009. download

Research Reports

  1. Xavier Leroy, W, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. Research Report INRIA, No 0, June 2012. download