The ProVal team was stopped at the end of August 2012, and reborn into a new team
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Publications : Yannick MoyBack
Claire Dross, Jean-Christophe Filliâtre, and Yannick Moy.
Correct Code Containing Containers.
In 5th International Conference on Tests and Proofs (TAP'11),
volume 6706 of Lecture Notes in Computer Science, pages 102-118,
Zurich, June 2011. Springer.
[ bib |
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.
|||Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in Frama-C - Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib | PDF | http ]|
|||Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ]|
|||Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184-1211, 2010. [ bib | DOI | full paper on HAL ]|
|||Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ]|
|||Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ]|
|||Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]|
|||Yannick Moy. Sufficient preconditions for modular assertion checking. In Francesco Logozzo, Doron Peled, and Lenore Zuck, editors, 9th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 4905 of Lecture Notes in Computer Science, pages 188-202, San Francisco, California, USA, January 2008. Springer. [ bib | PDF | .pdf ]|
|||Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ]|
|||Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]|
|||Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ]|
|||Yannick Moy. Union and cast in deductive verification. In Proceedings of the C/C++ Verification Workshop, volume Technical Report ICIS-R07015, pages 1-16. Radboud University Nijmegen, July 2007. [ bib | PDF | .pdf ]|
|||Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), pages 35-51, Braga, Portugal, March 2007. [ bib | PDF | .pdf ]|
This page was generated by bibtex2html.