Claude Marché

Publication Activity (10 Years)

Years Active: 1990-2022
Publications (10 Years): 17

Top Topics

Automated Verification

Software Packages

Top Venues

Int. J. Softw. Tools Technol. Transf.

J. Log. Algebraic Methods Program.

Publications

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
Automated formal analysis of temporal properties of Ladder programs. Int. J. Softw. Tools Technol. Transf. 24 (6) (2022)
Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
The CoLiS platform for the analysis of maintainer scripts in Debian software packages. Int. J. Softw. Tools Technol. Transf. 24 (5) (2022)
Xavier Denis, Jacques-Henri Jourdan, Claude Marché
Creusot: A Foundry for the Deductive Verification of Rust Programs. ICFEM (2022)
Benedikt F. H. Becker, Cláudio Belo Lourenço, Claude Marché
Explaining Counterexamples with Giant-Step Assertion Checking. F-IDE@NFM (2021)
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
Automated Verification of Temporal Properties of Ladder Programs. FMICS (2021)
Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
Analysing installation scenarios of Debian packages. TACAS (2) (2020)
Martin Clochard, Claude Marché, Andrei Paskevich
Deductive verification with ghost monitors. Proc. ACM Program. Lang. 4 (POPL) (2020)
Benedikt F. H. Becker, Claude Marché
Ghost Code in Action: Automated Verification of a Symbolic Interpreter. VSTTE (2019)
Sylvain Dailler, Claude Marché, Yannick Moy
Lightweight Interactive Proving inside an Automatic Program Verifier. F-IDE@FLoC (2018)
Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy
Instrumenting a weakest precondition calculus for counterexample generation. J. Log. Algebraic Methods Program. 99 (2018)
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. VSTTE (2017)
Clément Fumex, Claude Marché, Yannick Moy
Automating the Verification of Floating-Point Programs. VSTTE (2017)
Nicolas Jeannerod, Claude Marché, Ralf Treinen
A Formally Verified Interpreter for a Shell-Like Programming Language. VSTTE (2017)
Ran Chen, Martin Clochard, Claude Marché
A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. J. Formaliz. Reason. 10 (1) (2017)
Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché
Specification and Proof of High-Level Functional Properties of Bit-Level Programs. NFM (2016)
David Hauzar, Claude Marché, Yannick Moy
Counterexamples from Proof Failures in SPARK. SEFM (2016)
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) (2016)
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
Let's verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17 (6) (2015)
Claude Marché, Johannes Kanig
Bridging the Gap between Testing and Formal Verification in Ada Development. ERCIM News 2015 (100) (2015)
David Delahaye, Catherine Dubois, Claude Marché, David Mentré
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. ABZ (2014)
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
Formalizing Semantics with an Automatic Program Verifier. VSTTE (2014)
Martin Clochard, Claude Marché, Andrei Paskevich
Verified programs with binders. PLPV (2014)
Claude Marché
Verification of the functional behavior of a floating-point program: An industrial case study. Sci. Comput. Program. 96 (2014)
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
Preserving User Proofs across Specification Changes. VSTTE (2013)
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. ABZ (2012)
Paolo Herms, Claude Marché, Benjamin Monate
A Certified Multi-prover Verification Condition Generator. VSTTE (2012)
Thi Minh Tuyen Nguyen, Claude Marché
Hardware-Dependent Proofs of Numerical Programs. CPP (2011)
Sylvie Boldo, Claude Marché
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. Math. Comput. Sci. 5 (4) (2011)
Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich
The COST IC0701 Verification Competition 2011. FoVeOOS (2011)
Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko
Specifying generic Java programs: two case studies. LDTA (2010)
Yannick Moy, Claude Marché
Modular inference of subprogram contracts for safety checking. J. Symb. Comput. 45 (11) (2010)
Asma Tafat, Sylvain Boulmé, Claude Marché
A Refinement Methodology for Object-Oriented Programs. FoVeOOS (2010)
Ali Ayad, Claude Marché
Multi-Prover Verification of Floating-Point Programs. IJCAR (2010)
Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain
Proving operational termination of membership equational programs. High. Order Symb. Comput. 21 (1-2) (2008)
Claude Marché
Jessie: an intermediate language for Java and C verification. PLPV (2007)
Claude Marché, Hans Zantema
The Termination Competition. RTA (2007)
Jean-Christophe Filliâtre, Claude Marché
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. CAV (2007)
Claude Marché
Towards Modular Algebraic Specifications for Pointer Programs: A Case Study. Rewriting, Computation and Proof (2007)
Claude Marché, Nicolas Rousset
Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears. SEFM (2006)
Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain
Mechanically Proving Termination Using Polynomial Interpretations. J. Autom. Reason. 34 (4) (2005)
Claude Marché, Christine Paulin-Mohring
Reasoning About Java Programs with Aliasing and Frame Conditions. TPHOLs (2005)
Thierry Hubert, Claude Marché
A case study of C source code verification: the Schorr-Waite algorithm. SEFM (2005)
Salvador Lucas, Claude Marché, José Meseguer
Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95 (4) (2005)
Bart Jacobs, Claude Marché, Nicole Rauch
Formal Verification of a Commercial Smart Card Applet with Multiple Tools. AMAST (2004)
Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, Xavier Urbain
Proving termination of membership equational programs. PEPM (2004)
Claude Marché, Xavier Urbain
Modular and incremental proofs of AC-termination. J. Symb. Comput. 38 (1) (2004)
Jean-Christophe Filliâtre, Claude Marché
Multi-prover Verification of C Programs. ICFEM (2004)
Claude Marché, Christine Paulin-Mohring, Xavier Urbain
The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. J. Log. Algebraic Methods Program. 58 (1-2) (2004)
Claude Marché, Benoit Robert
Dam Failure Risk: Its Definition and Impact on Safety Assessment of Dam Structures. J. Decis. Syst. 11 (3-4) (2002)
Enno Ohlebusch, Claus Claves, Claude Marché
TALP: A Tool for the Termination Analysis of Logic Programs. RTA (2000)
Claude Marché, Xavier Urbain
Termination of Associative-Commutative Rewriting by Dependency Pairs. RTA (1998)
Evelyne Contejean, Claude Marché, Landy Rabehasaina
Rewrite Systems for Natural, Integral, and Rational Arithmetic. RTA (1997)
Claude Marché
Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations. J. Symb. Comput. 21 (3) (1996)
Alexandre Boudet, Evelyne Contejean, Claude Marché
AC-Complete Unification and its Application to Theorem Proving. RTA (1996)
Evelyne Contejean, Claude Marché
. RTA (1996)
Claude Marché
Normalised Rewriting and Normalised Completion LICS (1994)
Claude Marché
Normalized Rewriting - Application to Ground Completion and Standard Bases. Term Rewriting (1993)
Claude Marché
The Word Problem of ACD-Ground Theories is Undecidable. Int. J. Found. Comput. Sci. 3 (1) (1992)
Jean-Pierre Jouannaud, Claude Marché
Termination and Completion Modulo Associativity, Commutativity and Identity. Theor. Comput. Sci. 104 (1) (1992)
Claude Marché
On Ground AC-Completion. RTA (1991)
Jean-Pierre Jouannaud, Claude Marché
Completion modulo Associativity, Commutativity and Identity (AC1). DISCO (1990)