Skip to Main content Skip to Navigation


...
hal-01617437v1  Journal articles
Martin ClochardLéon GondelmanMário Pereira. The Matrix Reproved
Journal of Automated Reasoning, Springer Verlag, 2018, 60 (3), pp.365-383. ⟨10.1007/s10817-017-9436-2⟩
...
hal-01067197v1  Conference papers
Martin ClochardJean-Christophe FilliâtreClaude MarchéAndrei Paskevich. Formalizing Semantics with an Automatic Program Verifier
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
...
hal-01067217v1  Conference papers
Martin Clochard. Automatically verified implementation of data structures based on AVL trees
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
...
hal-00920955v1  Conference papers
Swarat ChaudhuriMartin ClochardArmando Solar-Lezama. Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search
POPL - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States
...
hal-01094488v1  Conference papers
Martin ClochardLéon Gondelman. Double WP : Vers une preuve automatique d'un compilateur
Journées Francophones des Langages Applicatifs, Jan 2015, Val d'Ajol, France
...
hal-00913431v1  Conference papers
Martin ClochardClaude MarchéAndrei Paskevich. Verified Programs with Binders
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
...
hal-01404935v1  Conference papers
Martin Clochard. Preuves taillées en biseau
vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France
...
hal-01316902v2  Conference papers
Martin ClochardLéon GondelmanMário Pereira. The Matrix Reproved (Verification Pearl)
VSTTE 2016, Jul 2016, Toronto, Canada
...
hal-01652148v1  Journal articles
Ran ChenMartin ClochardClaude Marché. A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links
Journal of Formalized Reasoning, ASDD-AlmaDL, 2017, 10 (1)
...
hal-01907894v1  Reports
Martin ClochardAndrei PaskevichClaude Marché. Deductive Verification via Ghost Debugging
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
...
hal-01162661v2  Conference papers
Martin ClochardJean-Christophe FilliâtreAndrei Paskevich. How to avoid proving the absence of integer overflows
7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States
...
hal-02368284v1  Conference papers
Martin ClochardClaude MarchéAndrei Paskevich. Deductive Verification with Ghost Monitors
POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩