Wiki Agenda Contact Version française

Publications : Yannick Moy

Back
[18] Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer. [ bib | full text on HAL ]
[17] Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ]
[16] Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 9952 of Lecture Notes in Computer Science, pages 461--478, Corfu, Greece, October 2016. Springer. [ bib | full text on HAL ]
[15] David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria Saclay Ile-de-France, February 2016. [ bib | full text on HAL ]
[14] David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Software Engineering and Formal Methods, pages 215--233, 2016. [ bib | full text on HAL ]
[13] 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 | full text on HAL | .pdf ]
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.

[12] 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 ]
[11] Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ]
[10] Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184--1211, 2010. [ bib | DOI | full text on HAL ]
[9] 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 ]
[8] Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ]
[7] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[6] 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 ]
[5] 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 ]
[4] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[3] Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ]
[2] 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 ]
[1] 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 ]

Back
This page was generated by bibtex2html.