Publications : Yannick Moy
Retour| [34] | Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.16, 2020. [ bib | .html ] |
| [33] | Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. In Formal Methods and Software Engineering (ICFEM), pages 55--72, 2020. [ bib | DOI | full text on HAL ] |
| [32] | Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. working paper https://hal.inria.fr/hal-01936105, November 2018. [ bib | full text on HAL ] |
| [31] | Yannick Moy. Climbing the software assurance ladder - practical formal verification for reliable software. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 76, 2018. [ bib | DOI | http ] |
| [30] |
Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy.
Instrumenting a weakest precondition calculus for counterexample
generation.
Journal of Logical and Algebraic Methods in Programming,
99:97--113, 2018.
[ bib |
DOI |
full text on HAL ]
Keywords: Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples |
| [29] | Sylvain Dailler, Claude Marché, and Yannick Moy. Lightweight interactive proving inside an automatic program verifier. In Proceedings of the Fourth Workshop on Formal Integrated Development Environment, F-IDE, Oxford, UK, July 14, 2018, 2018. [ bib | DOI | full text on HAL ] |
| [28] | Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
| [27] | 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 ] |
| [26] | Claire Dross and Yannick Moy. Auto-active proof of red-black trees in spark. In NASA Formal Methods, 2017. [ bib ] |
| [25] | 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 | DOI | full text on HAL ] |
| [24] | 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 ] |
| [23] | Claire Dross and Yannick Moy. Abstract software specifications and automatic proof of refinement. In 1st International Conference on Reliability, Safety and Security of Railway Systems, 2016. [ bib ] |
| [22] | David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Rocco De Nicola and Eva Kühn, editors, Software Engineering and Formal Methods, Lecture Notes in Computer Science, pages 215--233, Vienna, Austria, 2016. [ bib | DOI | full text on HAL ] |
| [21] | Johannes Kanig, Rod Chapman, Cyrille Comar, Jerôme Guitton, Yannick Moy, and Emyr Rees. Explicit assumptions - a prenup for marrying static and dynamic program verification. In Martina Seidl and Nikolai Tillmann, editors, Tests and Proofs, 8th International Conference, volume 8570 of Lecture Notes in Computer Science, pages 142--157. Springer, 2014. [ bib | DOI ] |
| [20] | J.-C. Filliâtre, C. Marché, Y. Moy, and R. Bardou. Why version 2.30. APP Deposit, August 2012. IDDN.FR.001.350004.000.S.P.2012.000.10000. [ bib ] |
| [19] |
Cyrille Comar, Johannes Kanig, and Yannick Moy.
Integrating formal program verification with testing.
In Proceedings of the Embedded Real Time Software and Systems
conference, ERTS2 2012, February 2012.
[ bib ]
Keywords: GNATprove |
| [18] | Jérôme Guitton, Johannes Kanig, and Yannick Moy. Why Hi-Lite Ada? In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 27--39, Wroclaw, Poland, August 2011. [ bib ] |
| [17] |
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.
|
| [16] | Jérôme Guitton, Johannes Kanig, and Yannick Moy. Why Hi-Lite Ada? In Boogie, pages 27--39, 2011. [ bib ] |
| [15] | 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 ] |
| [14] | Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ] |
| [13] | 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 ] |
| [12] | 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 ] |
| [11] | Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ] |
| [10] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
| [9] | 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 ] |
| [8] | 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 ] |
| [7] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
| [6] | Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ] |
| [5] | 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 ] |
| [4] | 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 ] |
| [3] | D. Lugiez and J.L. Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of symbolic computation, 11(1), 1994. [ bib ] |
| [2] | D. Lugiez and J.-L. Moysset. Complement problems and tree automata in AC-like theories. In Proc. Symp. on Theoretical Aspects of Computer Science, Würzburg, 1993. also available as techincal report CRIN 92-R-175. [ bib ] |
| [1] | D. Lugiez and J.-L. Moysset. Tree automata help solve formulae in AC-theories. Research Report 93-RR-044, CRIN, Nancy, 1993. [ bib ] |
Retour
This page was generated by bibtex2html.