Completion modulo Associativity, Commutativity and Identity (AC1). - Jean-Pierre Jouannaud; Claude Marché (DISCO, 1990)

On Ground AC-Completion. - Claude Marché (RTA, 1991)

The Word Problem of ACD-Ground Theories is Undecidable. - Claude Marché (Int. J. Found. Comput. Sci., 1992)

Termination and Completion Modulo Associativity, Commutativity and Identity. - Jean-Pierre Jouannaud; Claude Marché (Theor. Comput. Sci., 1992)

Normalized Rewriting - Application to Ground Completion and Standard Bases. - Claude Marché (Term Rewriting, 1993)

Normalised Rewriting and Normalised Completion - Claude Marché (LICS, 1994)

AC-Complete Unification and its Application to Theorem Proving. - Alexandre Boudet; Evelyne Contejean; Claude Marché (RTA, 1996)

CiME: Completion Modulo E. - Evelyne Contejean; Claude Marché (RTA, 1996)

Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations. - Claude Marché (J. Symb. Comput., 1996)

Rewrite Systems for Natural, Integral, and Rational Arithmetic. - Evelyne Contejean; Claude Marché; Landy Rabehasaina (RTA, 1997)

Termination of Associative-Commutative Rewriting by Dependency Pairs. - Claude Marché; Xavier Urbain (RTA, 1998)

TALP: A Tool for the Termination Analysis of Logic Programs. - Enno Ohlebusch; Claus Claves; Claude Marché (RTA, 2000)

Dam Failure Risk: Its Definition and Impact on Safety Assessment of Dam Structures. - Claude Marché; Benoit Robert (J. Decis. Syst., 2002)

Formal Verification of a Commercial Smart Card Applet with Multiple Tools. - Bart Jacobs 001; Claude Marché; Nicole Rauch (AMAST, 2004)

Multi-prover Verification of C Programs. - Jean-Christophe Filliâtre; Claude Marché (ICFEM, 2004)

Proving termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Claude Marché; Xavier Urbain (PEPM, 2004)

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. - Claude Marché; Christine Paulin-Mohring; Xavier Urbain (J. Log. Algebraic Methods Program., 2004)

Modular and incremental proofs of AC-termination. - Claude Marché; Xavier Urbain (J. Symb. Comput., 2004)

A case study of C source code verification: the Schorr-Waite algorithm. - Thierry Hubert; Claude Marché (SEFM, 2005)

Reasoning About Java Programs with Aliasing and Frame Conditions. - Claude Marché; Christine Paulin-Mohring (TPHOLs, 2005)

Operational termination of conditional term rewriting systems. - Salvador Lucas; Claude Marché; José Meseguer 001 (Inf. Process. Lett., 2005)

Mechanically Proving Termination Using Polynomial Interpretations. - Evelyne Contejean; Claude Marché; Ana Paula Tomás; Xavier Urbain (J. Autom. Reason., 2005)

Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears. - Claude Marché; Nicolas Rousset (SEFM, 2006)

Towards Modular Algebraic Specifications for Pointer Programs: A Case Study. - Claude Marché (Rewriting, Computation and Proof, 2007)

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. - Jean-Christophe Filliâtre; Claude Marché (CAV, 2007)

Jessie: an intermediate language for Java and C verification. - Claude Marché (PLPV, 2007)

The Termination Competition. - Claude Marché; Hans Zantema (RTA, 2007)

Proving operational termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; Claude Marché; José Meseguer 001; Xavier Urbain (High. Order Symb. Comput., 2008)

Multi-Prover Verification of Floating-Point Programs. - Ali Ayad; Claude Marché (IJCAR, 2010)

A Refinement Methodology for Object-Oriented Programs. - Asma Tafat; Sylvain Boulmé; Claude Marché (FoVeOOS, 2010)

Specifying generic Java programs: two case studies. - Alain Giorgetti; Claude Marché; Elena Tushkanova; Olga Kouchnarenko (LDTA, 2010)

Modular inference of subprogram contracts for safety checking. - Yannick Moy; Claude Marché (J. Symb. Comput., 2010)

Hardware-Dependent Proofs of Numerical Programs. - Thi Minh Tuyen Nguyen; Claude Marché (CPP, 2011)

The COST IC0701 Verification Competition 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; et al. (FoVeOOS, 2011)

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. - Sylvie Boldo; Claude Marché (Math. Comput. Sci., 2011)

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. - David Mentré; Claude Marché; Jean-Christophe Filliâtre; Masashi Asuka (ABZ, 2012)

A Certified Multi-prover Verification Condition Generator. - Paolo Herms; Claude Marché; Benjamin Monate (VSTTE, 2012)

Preserving User Proofs across Specification Changes. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich (VSTTE, 2013)

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. - David Delahaye; Catherine Dubois; Claude Marché; David Mentré (ABZ, 2014)

Verified programs with binders. - Martin Clochard; Claude Marché; Andrei Paskevich (PLPV, 2014)

Formalizing Semantics with an Automatic Program Verifier. - Martin Clochard; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (VSTTE, 2014)

Verification of the functional behavior of a floating-point program: An industrial case study. - Claude Marché (Sci. Comput. Program., 2014)

Bridging the Gap between Testing and Formal Verification in Ada Development. - Claude Marché; Johannes Kanig (ERCIM News, 2015)

Let's verify this with Why3. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (Int. J. Softw. Tools Technol. Transf., 2015)

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. - Nikolai Kosmatov; Claude Marché; Yannick Moy; Julien Signoles (ISoLA (1), 2016)

Specification and Proof of High-Level Functional Properties of Bit-Level Programs. - Clément Fumex; Claire Dross; Jens Gerlach; Claude Marché (NFM, 2016)

Counterexamples from Proof Failures in SPARK. - David Hauzar; Claude Marché; Yannick Moy (SEFM, 2016)

Automating the Verification of Floating-Point Programs. - Clément Fumex; Claude Marché; Yannick Moy (VSTTE, 2017)

A Formally Verified Interpreter for a Shell-Like Programming Language. - Nicolas Jeannerod; Claude Marché; Ralf Treinen (VSTTE, 2017)

How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. - Raphaël Rieu-Helft; Claude Marché; Guillaume Melquiond (VSTTE, 2017)

A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. - Ran Chen; Martin Clochard; Claude Marché (J. Formaliz. Reason., 2017)

Lightweight Interactive Proving inside an Automatic Program Verifier. - Sylvain Dailler; Claude Marché; Yannick Moy (F-IDE@FLoC, 2018)

Instrumenting a weakest precondition calculus for counterexample generation. - Sylvain Dailler; David Hauzar; Claude Marché; Yannick Moy (J. Log. Algebraic Methods Program., 2018)

Ghost Code in Action: Automated Verification of a Symbolic Interpreter. - Benedikt F. H. Becker; Claude Marché (VSTTE, 2019)

Analysing installation scenarios of Debian packages. - Benedikt F. H. Becker; Nicolas Jeannerod; Claude Marché; Yann Régis-Gianas; Mihaela Sighireanu; Ralf Treinen (TACAS (2), 2020)

Deductive verification with ghost monitors. - Martin Clochard; Claude Marché; Andrei Paskevich (Proc. ACM Program. Lang., 2020)

Automated Verification of Temporal Properties of Ladder Programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (FMICS, 2021)

Explaining Counterexamples with Giant-Step Assertion Checking. - Benedikt F. H. Becker; Cláudio Belo Lourenço; Claude Marché (F-IDE@NFM, 2021)

Creusot: A Foundry for the Deductive Verification of Rust Programs. - Xavier Denis; Jacques-Henri Jourdan; Claude Marché (ICFEM, 2022)

The CoLiS platform for the analysis of maintainer scripts in Debian software packages. - Benedikt F. H. Becker; Nicolas Jeannerod; Claude Marché; Yann Régis-Gianas; Mihaela Sighireanu; Ralf Treinen (Int. J. Softw. Tools Technol. Transf., 2022)

Automated formal analysis of temporal properties of Ladder programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (Int. J. Softw. Tools Technol. Transf., 2022)

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. - Paul Bonnot; Benoît Boyer; Florian Faissole; Claude Marché; Raphaël Rieu-Helft (FMCAD, 2024)