Publications : Martin Clochard
Retour| [15] | Martin Clochard, Claude Marché, and Andrei Paskevich. Deductive verification with ghost monitors. In Principles of Programming Languages, New Orleans, United States, 2020. [ bib | DOI | full text on HAL ] |
| [14] | Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de doctorat, Université Paris-Saclay, March 2018. [ bib | full text on HAL ] |
| [13] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. Journal of Automated Reasoning, 60(3):365--383, 2018. [ bib | DOI | full text on HAL ] |
| [12] | Martin Clochard, Andrei Paskevich, and Claude Marché. Deductive verification via ghost debugging. Research Report 9219, Inria, 2018. [ bib | full text on HAL ] |
| [11] | Martin Clochard. Preuves taillées en biseau. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
| [10] | Ran Chen, Martin Clochard, and Claude Marché. A formally proved, complete algorithm for path resolution with symbolic links. Journal of Formalized Reasoning, 10(1):51--66, 2017. [ bib | DOI | full text on HAL | http ] |
| [9] | Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016. [ bib | full text on HAL ] |
| [8] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib | full text on HAL ] |
| [7] |
Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich.
How to avoid proving the absence of integer overflows.
In Arie Gurfinkel and Sanjit A. Seshia, editors, 7th Working
Conference on Verified Software: Theories, Tools and Experiments (VSTTE),
volume 9593 of Lecture Notes in Computer Science, pages 94--109, San
Francisco, California, USA, July 2015. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [6] | Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib | full text on HAL ] |
| [5] |
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Formalizing semantics with an automatic program verifier.
In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th
Working Conference on Verified Software: Theories, Tools and Experiments
(VSTTE), volume 8471 of Lecture Notes in Computer Science, pages
37--51, Vienna, Austria, July 2014. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [4] |
Martin Clochard.
Automatically verified implementation of data structures based on
AVL trees.
In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th
Working Conference on Verified Software: Theories, Tools and Experiments
(VSTTE), volume 8471 of Lecture Notes in Computer Science, pages
167--180, Vienna, Austria, July 2014. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [3] | Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages meets Program Verification (PLPV). ACM Press, 2014. [ bib | full text on HAL ] |
| [2] | M. Clochard, S. Chaudhuri, and A. Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ] |
| [1] | Martin Clochard. Proving programs with binders, automatically. Master's thesis, Master Parisien de Recherche en Informatique, 2013. [ bib ] |
Retour
This page was generated by bibtex2html.