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. Masci, Paolo; Monahan, Rosemary; Prevosto, Virgile. 4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom. Open Publishing Association, 284, 2018, Electronic Proceedings in Theoretical Computer Science. 〈hal-01936302〉

Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. Andrei Paskevich; Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. 10712, pp.84-101, 2017, Lecture Notes in Computer Science. 〈https://vstte17.lri.fr/〉. 〈10.1007/978-3-319-72308-2_6〉. 〈hal-01519732v2〉

Clément Fumex, Claude Marché, Yannick Moy. Automating the Verification of Floating-Point Programs. Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 10712, 2017, Lecture Notes in Computer Science. 〈http://vstte17.lri.fr/〉. 〈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. 10712, 2017, Lecture Notes in Computer Science. 〈hal-01534747〉

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. Springer, 2016, NASA Formal methods. 〈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. Springer, 9952, pp.461--478, 2016, Lecture Notes in Computer Science. 〈hal-01344110〉

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

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

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. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science. 〈hal-00998092〉

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. EasyChair, 2014. 〈hal-00998094〉

Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier. Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science. 〈hal-01067197〉

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

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

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〉

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. Springer, 7421, 2012, Lecture Notes in Computer Science. 〈hal-00789525〉

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, 2011. 〈hal-00790310〉

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

Ali Ayad, Claude Marché. Multi-prover verification of floating-point programs. Jürgen Giesl and Reiner Hähnle. Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6173, 2010, Lecture Notes in Artificial Intelligence. 〈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, 2010. 〈inria-00525784〉

Asma Tafat, Sylvain Boulmé, Claude Marché. A refinement methodology for object-oriented programs. Bernhard Beckert and Claude Marché. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. Karlsruhe University, 2010-13, pp.143--159, 2010, Karlsruhe Reports in Informatics. 〈inria-00534336〉

Jean-Christophe Filliâtre, Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. Werner Damm and Holger Hermanns. 19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany. 2007, Lecture Notes in Computer Science. 〈inria-00270820〉

Claude Marché, Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. Dang Van Hung, Paritosh Pandya. Software Engineering and Formal Methods, Sep 2006, Pune, India. IEEE Comp. Soc. Press, 2006, th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06). 〈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. Tutorial and Reference Manual. 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〉

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

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

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〉

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

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

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〉

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〉