Claude Marché

According to our database, Claude Marché authored at least 61 papers between 1990 and 2022.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2022

Automated formal analysis of temporal properties of Ladder programs.

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Int. J. Softw. Tools Technol. Transf., 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

Creusot: A Foundry for the Deductive Verification of Rust Programs.

Xavier Denis, Jacques-Henri Jourdan, Claude Marché

Proceedings of the Formal Methods and Software Engineering, 2022

2021

Explaining Counterexamples with Giant-Step Assertion Checking.

Benedikt F. H. Becker, Cláudio Belo Lourenço, Claude Marché

Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Automated Verification of Temporal Properties of Ladder Programs.

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Proceedings of the Formal Methods for Industrial Critical Systems, 2021

2020

Deductive verification with ghost monitors.

Martin Clochard, Claude Marché, Andrei Paskevich

Proc. ACM Program. Lang., 2020

Analysing installation scenarios of Debian packages.

Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

2019

Ghost Code in Action: Automated Verification of a Symbolic Interpreter.

Benedikt F. H. Becker, Claude Marché

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2019

2018

Instrumenting a weakest precondition calculus for counterexample generation.

Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy

J. Log. Algebraic Methods Program., 2018

Lightweight Interactive Proving inside an Automatic Program Verifier.

Sylvain Dailler, Claude Marché, Yannick Moy

Proceedings of the Proceedings 4th Workshop on Formal Integrated Development Environment, 2018

2017

A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links.

Ran Chen, Martin Clochard, Claude Marché

J. Formaliz. Reason., 2017

How to Get an Efficient yet Verified Arbitrary-Precision Integer Library.

Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

A Formally Verified Interpreter for a Shell-Like Programming Language.

Nicolas Jeannerod, Claude Marché, Ralf Treinen

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

Automating the Verification of Floating-Point Programs.

Clément Fumex, Claude Marché, Yannick Moy

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

2016

Counterexamples from Proof Failures in SPARK.

David Hauzar, Claude Marché, Yannick Moy

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Specification and Proof of High-Level Functional Properties of Bit-Level Programs.

Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.

Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

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

Bridging the Gap between Testing and Formal Verification in Ada Development.

Claude Marché, Johannes Kanig

ERCIM News, 2015

2014

Verification of the functional behavior of a floating-point program: An industrial case study.

Claude Marché

Sci. Comput. Program., 2014

Formalizing Semantics with an Automatic Program Verifier.

Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Verified programs with binders.

Martin Clochard, Claude Marché, Andrei Paskevich

Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations.

David Delahaye, Catherine Dubois, Claude Marché, David Mentré

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013

Preserving User Proofs across Specification Changes.

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

2012

A Certified Multi-prover Verification Condition Generator.

Paolo Herms, Claude Marché, Benjamin Monate

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers.

David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

2011

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs.

Sylvie Boldo, Claude Marché

Math. Comput. Sci., 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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich

Proceedings of the Formal Verification of Object-Oriented Software, 2011

Hardware-Dependent Proofs of Numerical Programs.

Thi Minh Tuyen Nguyen, Claude Marché

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Modular inference of subprogram contracts for safety checking.

Yannick Moy, Claude Marché

J. Symb. Comput., 2010

Specifying generic Java programs: two case studies.

Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko

Proceedings of the of the Tenth Workshop on Language Descriptions, Tools and Applications, 2010

A Refinement Methodology for Object-Oriented Programs.

Asma Tafat, Sylvain Boulmé, Claude Marché

Proceedings of the Formal Verification of Object-Oriented Software, 2010

Multi-Prover Verification of Floating-Point Programs.

Ali Ayad, Claude Marché

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2008

Proving operational termination of membership equational programs.

Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain

High. Order Symb. Comput., 2008

2007

The Termination Competition.

Claude Marché, Hans Zantema

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Jessie: an intermediate language for Java and C verification.

Claude Marché

Proceedings of the ACM Workshop Programming Languages meets Program Verification, 2007

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.

Jean-Christophe Filliâtre, Claude Marché

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Towards Modular Algebraic Specifications for Pointer Programs: A Case Study.

Claude Marché

Proceedings of the Rewriting, 2007

2006

Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears.

Claude Marché, Nicolas Rousset

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

2005

Mechanically Proving Termination Using Polynomial Interpretations.

Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain

J. Autom. Reason., 2005

Operational termination of conditional term rewriting systems.

Salvador Lucas, Claude Marché, José Meseguer

Inf. Process. Lett., 2005

Reasoning About Java Programs with Aliasing and Frame Conditions.

Claude Marché, Christine Paulin-Mohring

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

A case study of C source code verification: the Schorr-Waite algorithm.

Thierry Hubert, Claude Marché

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

2004

Modular and incremental proofs of AC-termination.

Claude Marché, Xavier Urbain

J. Symb. Comput., 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

Proving termination of membership equational programs.

Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, Xavier Urbain

Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Multi-prover Verification of C Programs.

Jean-Christophe Filliâtre, Claude Marché

Proceedings of the Formal Methods and Software Engineering, 2004

Formal Verification of a Commercial Smart Card Applet with Multiple Tools.

Bart Jacobs, Claude Marché, Nicole Rauch

Proceedings of the Algebraic Methodology and Software Technology, 2004

2002

Dam Failure Risk: Its Definition and Impact on Safety Assessment of Dam Structures.

Claude Marché, Benoit Robert

J. Decis. Syst., 2002

2000

TALP: A Tool for the Termination Analysis of Logic Programs.

Enno Ohlebusch, Claus Claves, Claude Marché

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1998

Termination of Associative-Commutative Rewriting by Dependency Pairs.

Claude Marché, Xavier Urbain

Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

1997

Rewrite Systems for Natural, Integral, and Rational Arithmetic.

Evelyne Contejean, Claude Marché, Landy Rabehasaina

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

1996

Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations.

Claude Marché

J. Symb. Comput., 1996

C<i>i</i>ME: Complet<i>i</i>on Modulo <i>E</i>.

Evelyne Contejean, Claude Marché

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

AC-Complete Unification and its Application to Theorem Proving.

Alexandre Boudet, Evelyne Contejean, Claude Marché

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1994

Normalised Rewriting and Normalised Completion

Claude Marché

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

1993

Normalized Rewriting - Application to Ground Completion and Standard Bases.

Claude Marché

Proceedings of the Term Rewriting, 1993

1992

Termination and Completion Modulo Associativity, Commutativity and Identity.

Jean-Pierre Jouannaud, Claude Marché

Theor. Comput. Sci., 1992

The Word Problem of ACD-Ground Theories is Undecidable.

Claude Marché

Int. J. Found. Comput. Sci., 1992

1991

On Ground AC-Completion.

Claude Marché

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990

Completion modulo Associativity, Commutativity and Identity (AC1).

Jean-Pierre Jouannaud, Claude Marché

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1990