Wiki Agenda Contact English version

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.