Claude Marché

Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2022. ⟨hal-03737886⟩

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Automated Formal Analysis of Temporal Properties of Ladder Programs. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2022. ⟨hal-03737869⟩

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. ⟨hal-01102242⟩

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3. International Journal on Software Tools for Technology Transfer, Springer Verlag, 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é, 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⟩

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

Xavier Denis, Jacques-Henri Jourdan, Claude Marché. Creusot: a Foundry for the Deductive Verication of Rust Programs. International Conference on Formal Engineering Methods - ICFEM, Oct 2022, Madrid, Spain. ⟨hal-03737878⟩

Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. Explaining Counterexamples with Giant-Step Assertion Checking. F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩. ⟨hal-03217393⟩

Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Automated Verification of Temporal Properties of Ladder Programs. FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩. ⟨hal-03281580⟩

Diego Diverio, Cláudio Lourenço, Claude Marché. You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3. VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7. ⟨hal-03002187⟩

Martin Clochard, Claude 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⟩. ⟨hal-02368284⟩

Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich. Des transformations logiques passent leur certificat. JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02384946v2⟩

Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. Analysing installation scenarios of Debian packages. TACAS 2020 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩. ⟨hal-02355602v2⟩

Benedikt Becker, Claude Marché. Ghost Code in Action: Automated Verification of a Symbolic Interpreter. VSTTE 2019 - 11th Working Conference on Verified Software: Tools, Techniques and Experiments, Jul 2019, New York, United States. ⟨10.1007/978-3-030-41600-3_8⟩. ⟨hal-02276257⟩

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⟩

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⟩

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⟩

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, 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, Claude Marché, Andrei Paskevich. Verified Programs with Binders. Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ⟨hal-00913431⟩

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⟩

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⟩

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. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. ⟨hal-00681781⟩

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⟩

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

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⟩

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⟩

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⟩

Thierry Hubert, Claude Marché. Separation Analysis for Weakest Precondition-based Verification. HAV 2007 - Heap Analysis and Verication, Mar 2007, Braga, Portugal. pp.81--93. ⟨hal-03630177⟩

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⟩

Claude Marché, Christine Paulin-Mohring. Reasoning about Java Programs with Aliasing and Frame Conditions. Theorem Proving in Higher Order Logics, 2005, Oxford, United Kingdom. pp.179-194, ⟨10.1007/11541868_12⟩. ⟨hal-03274993⟩

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⟩

Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot. Why3 version 1.0. France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018. ⟨hal-03136256⟩

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⟩

Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. Giant-step Semantics for the Categorisation of Counterexamples. [Research Report] RR-9407, Inria. 2021, pp.43. ⟨hal-03213438⟩

Xavier Denis, Jacques-Henri Jourdan, Claude Marché. The CREUSOT Environment for the Deductive Verification of Rust Programs. [Research Report] RR-9448, Inria Saclay - Île de France. 2021. ⟨hal-03526634v2⟩

Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Formal Analysis of Ladder Programs using Deductive Verification. [Research Report] RR-9402, Inria. 2021, pp.25. ⟨hal-03199464⟩

Benedikt Becker, Jean-Christophe Filliâtre, Claude Marché. Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup. [Rapport Technique] Université Paris-Saclay. 2020. ⟨hal-02447409⟩

Benedikt Becker, Nicolas Jeannerod, Claude Marché, Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. [Technical Report] ANR. 2019. ⟨hal-02321743⟩

Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen. Specification of UNIX Utilities. [Technical Report] ANR. 2019. ⟨hal-02321691⟩

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

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⟩

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⟩

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⟩

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, Claude Marché. Binary Heaps Formally Verified in Why3. [Research Report] RR-7780, INRIA. 2011, pp.33. ⟨inria-00636083⟩

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

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⟩