Claude Marché

Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy. Instrumenting a Weakest Precondition Calculus for Counterexample Generation. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2018, 99, pp.97-113. ⟨hal-01802488⟩

Ran Chen, Martin Clochard, Claude Marché. A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. Journal of Formalized Reasoning, ASDD-AlmaDL, 2017, 10 (1). ⟨hal-01652148⟩

Claude Marché, Johannes Kanig. Bridging the Gap between Testing and Formal Verification in Ada Development. ERCIM News, ERCIM, 2015, 100, pp.2. ⟨http://ercim-news.ercim.eu/⟩. ⟨hal-01102242⟩

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3. Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩. ⟨hal-00967132⟩

Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study. Science of Computer Programming, Elsevier, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩. ⟨hal-00967124⟩

Sylvie Boldo, Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, Springer, 2011, 5, pp.377-393. ⟨hal-00777605⟩

Yannick Moy, Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, Elsevier, 2010, 45, pp.1184-1211. ⟨inria-00534331⟩

Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain. Proving Operational Termination of Membership Equational Programs. Higher-Order and Symbolic Computation, Springer Verlag, 2008, 21 (1-2), pp.59-88. ⟨inria-00431474⟩

Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain. Mechanically Proving Termination Using Polynomial Interpretations. Journal of Automated Reasoning, Springer Verlag, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩. ⟨hal-01984434⟩

Claude Marché, Christine Paulin-Mohring, Xavier Urbain. The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. The Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩. ⟨hal-01984932⟩

Claude Marché, Xavier Urbain. Modular and Incremental Proofs of AC-Termination. Journal of Symbolic Computation, Elsevier, 2004, 38 (1), pp.873-897. ⟨10.1016/j.jsc.2004.02.003⟩. ⟨hal-01984429⟩

Sylvain Dailler, Claude Marché, Yannick Moy. Lightweight Interactive Proving inside an Automatic Program Verifier. 4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom. ⟨hal-01936302⟩

Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩. ⟨hal-01519732v2⟩

Clément Fumex, Claude Marché, Yannick Moy. Automating the Verification of Floating-Point Programs. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. ⟨hal-01534533⟩

Nicolas Jeannerod, Claude Marché, Ralf Treinen. A Formally Verified Interpreter for a Shell-like Programming Language. VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. ⟨hal-01534747⟩

David Hauzar, Claude Marché, Yannick Moy. Counterexamples from Proof Failures in SPARK. Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. ⟨hal-01314885⟩

Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché. Specification and Proof of High-Level Functional Properties of Bit-Level Programs. NASA Formal methods, Jun 2016, Minneapolis, United States. ⟨hal-01314876⟩

Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478. ⟨hal-01344110⟩

David Delahaye, Claude Marché, David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B. Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France. ⟨hal-00998094⟩

David Delahaye, Catherine Dubois, Claude Marché, David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293. ⟨hal-00998092⟩

Martin Clochard, Jean-Christophe Filliâtre, Claude 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-01067197⟩

Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders. Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ⟨hal-00913431⟩

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Preserving User Proofs Across Specification Changes. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201. ⟨hal-00875395⟩

Claude Marché, Asma Tafat. Calcul de plus faible précondition, revisité en Why3. JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00778791⟩

David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka. Discharging Proof Obligations from Atelier B using Multiple Automated Provers. Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012. 〈hal-00681781〉

Thi Minh Tuyen Nguyen, Claude Marché. Hardware-Dependent Proofs of Numerical Programs. Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. ⟨hal-00772508⟩

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Why3: Shepherd Your Herd of Provers. Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64. ⟨hal-00790310⟩

Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, et al.. The COST IC0701 Verification Competition 2011. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy. ⟨hal-00789525⟩

Ali Ayad, Claude Marché. Multi-prover verification of floating-point programs. Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00534333⟩

Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko. Specifying Generic Java Programs: two case studies. 11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106. ⟨inria-00525784⟩

Asma Tafat, Sylvain Boulmé, Claude Marché. A refinement methodology for object-oriented programs. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159. ⟨inria-00534336⟩

Jean-Christophe Filliâtre, Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. 19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany. ⟨inria-00270820⟩

Claude Marché, Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. Software Engineering and Formal Methods, Sep 2006, Pune, India. ⟨inria-00129055⟩

Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché. Formal proofs of numerical programs. Forum Digitéo, Oct 2010, Palaiseau, France. ⟨inria-00536135⟩

Claude Marché. Towards Modular Algebraic Specifications for Pointer Programs: a Case Study. Hubert Comon-Lundh and Claude Kirchner and Hélène Kirchner. Rewriting, Computation and Proof, 4600, Springer, pp.235-258, 2007, lecture notes in computer science. ⟨inria-00431399⟩

Bernhard Beckert, Claude Marché. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010. Bernhard Beckert and Claude Marché. 6528, Springer, pp.200, 2011. ⟨hal-00772519⟩

Bernhard Beckert, Claude Marché. Formal Verification of Object-Oriented Software, Papers Presented at the International Conference. Bernhard Beckert and Claude Marché. 2010-13, Karlsruhe University, pp.368, 2010, Karlsruhe Reports in Informatics. ⟨inria-00534339⟩

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81. 2013. ⟨hal-00822856⟩

Martin Clochard, Claude Marché, Andrei Paskevich. Deductive Verification with Ghost Monitors. 2018. ⟨hal-01926659⟩

Martin Clochard, Andrei Paskevich, Claude Marché. Deductive Verification via Ghost Debugging. [Research Report] RR-9219, Inria Saclay Ile de France. 2018. ⟨hal-01907894⟩

Clément Fumex, Claude Marché, Yannick Moy. Automated Verification of Floating-Point Computations in Ada Programs. [Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53. ⟨hal-01511183⟩

Ilham Dami, Claude Marché. Le langage CoLiS : syntaxe, sémantique et outillage. [Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22. ⟨hal-01614488⟩

Ran Chen, Martin Clochard, Claude Marché. A Formal Proof of a Unix Path Resolution Algorithm. [Research Report] RR-8987, Inria. 2016, pp.27. ⟨hal-01406848⟩

David Hauzar, Claude Marché, Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. [Research Report] RR-8854, Inria. 2016, pp.22. ⟨hal-01271174⟩

Claire Dross, Clément Fumex, Jens Gerlach, Claude Marché. High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs. [Research Report] RR-8821, Inria Saclay. 2015, pp.52. ⟨hal-01238376⟩

Claude Marché, Asma Tafat. Weakest Precondition Calculus, Revisited using Why3. [Research Report] RR-8185, INRIA. 2012, pp.32. ⟨hal-00766171⟩

Nguyen Thi Minh Tuyen, Claude Marché. Proving Floating-Point Numerical Programs by Analysis of their Assembly Code. [Research Report] RR-7655, INRIA. 2011, pp.61. ⟨inria-00602266⟩

Krishnamani Kalyanasundaram, Claude Marché. Automated Generation of Loop Invariants using Predicate Abstraction. [Research Report] RR-7714, INRIA. 2011, pp.32. ⟨inria-00615623⟩

Asma Tafat, Claude Marché. Binary Heaps Formally Verified in Why3. [Research Report] RR-7780, INRIA. 2011, pp.33. ⟨inria-00636083⟩

Paolo Herms, Claude Marché, Benjamin Monate. A Certified Multi-prover Verification Condition Generator. [Research Report] RR-7793, INRIA. 2011, pp.22. ⟨hal-00639977⟩

Asma Tafat, Sylvain Boulmé, Claude Marché. A Refinement Approach for Correct-by-Construction Object-Oriented Programs. [Research Report] RR-7310, INRIA. 2010, pp.31. ⟨inria-00491835⟩

Romain Bardou, Claude Marché. Regions and Permissions for Verifying Data Invariants. [Research Report] RR-7412, INRIA. 2010, pp.40. ⟨inria-00525384⟩

Elena Tushkanova, Alain Giorgetti, Claude Marché, Olga Kouchnarenko. Modular Specification of Java Programs. [Research Report] RR-7097, INRIA. 2009, pp.26. ⟨inria-00434452⟩

Evelyne Contejean, Claude Marché, Ana-Paula Tomas, Xavier Urbain. Mechanically proving termination using polynomial interpretations. [Intern report] 1382, 2006. ⟨inria-00001167⟩