Wiki Agenda Contact English version

Publications : Martin Clochard

Retour
[10] Martin Clochard. Preuves taillées en biseau. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[9] Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a unix path resolution algorithm. Research Report RR-8987, Inria Saclay Ile-de-France, 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), Lecture Notes in Computer Science, 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.