Accéder directement au contenu

Claude Marché

78
Documents

Publications

Image document

The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages

Benedikt Becker , Nicolas Jeannerod , Claude Marché , Yann Régis-Gianas , Mihaela Sighireanu
International Journal on Software Tools for Technology Transfer, 2022
Article dans une revue hal-03737886v1
Image document

Automated Formal Analysis of Temporal Properties of Ladder Programs

Cláudio Belo Lourenço , Denis Cousineau , Florian Faissole , Claude Marché , David Mentré
International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
Article dans une revue hal-03737869v1
Image document

Instrumenting a Weakest Precondition Calculus for Counterexample Generation

Sylvain Dailler , David Hauzar , Claude Marché , Yannick Moy
Journal of Logical and Algebraic Methods in Programming, 2018, 99, pp.97-113
Article dans une revue hal-01802488v1
Image document

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

Ran Chen , Martin Clochard , Claude Marché
Journal of Formalized Reasoning, 2017, 10 (1)
Article dans une revue hal-01652148v1

Bridging the Gap between Testing and Formal Verification in Ada Development

Claude Marché , Johannes Kanig
ERCIM News, 2015, 100, pp.2
Article dans une revue hal-01102242v1
Image document

Let's Verify This with Why3

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
International Journal on Software Tools for Technology Transfer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
Article dans une revue hal-00967132v1
Image document

Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study

Claude Marché
Science of Computer Programming, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩
Article dans une revue hal-00967124v1
Image document

Formal verification of numerical programs: from C annotated programs to mechanical proofs

Sylvie Boldo , Claude Marché
Mathematics in Computer Science, 2011, 5, pp.377-393
Article dans une revue hal-00777605v1
Image document

Modular inference of subprogram contracts for safety checking

Yannick Moy , Claude Marché
Journal of Symbolic Computation, 2010, 45, pp.1184-1211
Article dans une revue inria-00534331v1
Image document

Proving Operational Termination of Membership Equational Programs

Francisco Durán , Salvador Lucas , Claude Marché , José Meseguer , Xavier Urbain
Higher-Order and Symbolic Computation, 2008, 21 (1-2), pp.59-88
Article dans une revue inria-00431474v1

Mechanically Proving Termination Using Polynomial Interpretations

Evelyne Contejean , Claude Marché , Ana Paula Tomás , Xavier Urbain
Journal of Automated Reasoning, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩
Article dans une revue hal-01984434v1

Modular and Incremental Proofs of AC-Termination

Claude Marché , Xavier Urbain
Journal of Symbolic Computation, 2004, 38 (1), pp.873-897. ⟨10.1016/j.jsc.2004.02.003⟩
Article dans une revue hal-01984429v1

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML

Claude Marché , Christine Paulin-Mohring , Xavier Urbain
Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩
Article dans une revue hal-01984932v1
Image document

De l'avantage de nuancer les décisions binaires

Claude Marché , Denis Cousineau
JFLA 2024 – 35es Journées Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France
Communication dans un congrès hal-04342273v2
Image document

Creusot: a Foundry for the Deductive Verification of Rust Programs

Xavier Denis , Jacques-Henri Jourdan , Claude Marché
ICFEM 2022 - 23th International Conference on Formal Engineering Methods, Oct 2022, Madrid, Spain
Communication dans un congrès hal-03737878v1
Image document

Automated Verification of Temporal Properties of Ladder Programs

Cláudio Lourenço , Denis Cousineau , Florian Faissole , Claude Marché , David Mentré
FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
Communication dans un congrès hal-03281580v1
Image document

Explaining Counterexamples with Giant-Step Assertion Checking

Benedikt Becker , Cláudio Belo Lourenço , Claude Marché
F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩
Communication dans un congrès hal-03217393v1
Image document

Deductive Verification with Ghost Monitors

Martin Clochard , Claude Marché , Andrei Paskevich
POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩
Communication dans un congrès hal-02368284v1
Image document

Des transformations logiques passent leur certificat

Quentin Garchery , Chantal Keller , Claude Marché , Andrei Paskevich
JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès hal-02384946v2
Image document

Analysing installation scenarios of Debian packages

Benedikt Becker , Nicolas Jeannerod , Claude Marché , Yann Régis-Gianas , Mihaela Sighireanu
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⟩
Communication dans un congrès hal-02355602v2
Image document

You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3

Diego Diverio , Cláudio Lourenço , Claude Marché
VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7
Communication dans un congrès hal-03002187v1
Image document

Ghost Code in Action: Automated Verification of a Symbolic Interpreter

Benedikt Becker , Claude Marché
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⟩
Communication dans un congrès hal-02276257v1
Image document

Lightweight Interactive Proving inside an Automatic Program Verifier

Sylvain Dailler , Claude Marché , Yannick Moy
4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom
Communication dans un congrès hal-01936302v1
Image document

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

Raphaël Rieu-Helft , Claude Marché , Guillaume Melquiond
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⟩
Communication dans un congrès hal-01519732v2
Image document

A Formally Verified Interpreter for a Shell-like Programming Language

Nicolas Jeannerod , Claude Marché , Ralf Treinen
VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany
Communication dans un congrès hal-01534747v1
Image document

Automating the Verification of Floating-Point Programs

Clément Fumex , Claude Marché , Yannick Moy
9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany
Communication dans un congrès hal-01534533v1
Image document

Counterexamples from Proof Failures in SPARK

David Hauzar , Claude Marché , Yannick Moy
Software Engineering and Formal Methods, Jul 2016, Vienna, Austria
Communication dans un congrès hal-01314885v1
Image document

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

Clément Fumex , Claire Dross , Jens Gerlach , Claude Marché
NASA Formal methods, Jun 2016, Minneapolis, United States
Communication dans un congrès hal-01314876v1
Image document

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

Nikolai Kosmatov , Claude Marché , Yannick Moy , Julien Signoles
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478
Communication dans un congrès hal-01344110v1
Image document

Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B

David Delahaye , Claude Marché , David Mentré
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France
Communication dans un congrès hal-00998094v1
Image document

Verified Programs with Binders

Martin Clochard , Claude Marché , Andrei Paskevich
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
Communication dans un congrès hal-00913431v1
Image document

Formalizing Semantics with an Automatic Program Verifier

Martin Clochard , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès hal-01067197v1
Image document

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

David Delahaye , Catherine Dubois , Claude Marché , David Mentré
Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293
Communication dans un congrès hal-00998092v1
Image document

Preserving User Proofs Across Specification Changes

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Guillaume Melquiond , Andrei Paskevich
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Communication dans un congrès hal-00875395v1
Image document

Calcul de plus faible précondition, revisité en Why3

Claude Marché , Asma Tafat
JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
Communication dans un congrès hal-00778791v1
Image document

Discharging Proof Obligations from Atelier B using Multiple Automated Provers

David Mentré , Claude Marché , Jean-Christophe Filliâtre , Masashi Asuka
ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy
Communication dans un congrès hal-00681781v1
Image document

The COST IC0701 Verification Competition 2011

Thorsten Bormer , Marc Brockschmidt , Dino Distefano , Gidon Ernst , Jean-Christophe Filliâtre
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy
Communication dans un congrès hal-00789525v1
Image document

Why3: Shepherd Your Herd of Provers

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Communication dans un congrès hal-00790310v1
Image document

Hardware-Dependent Proofs of Numerical Programs

Thi Minh Tuyen Nguyen , Claude Marché
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan
Communication dans un congrès hal-00772508v1
Image document

Multi-prover verification of floating-point programs

Ali Ayad , Claude Marché
Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00534333v1
Image document

A refinement methodology for object-oriented programs

Asma Tafat , Sylvain Boulmé , Claude Marché
Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159
Communication dans un congrès inria-00534336v1
Image document

Specifying Generic Java Programs: two case studies

Alain Giorgetti , Claude Marché , Elena Tushkanova , Olga Kouchnarenko
11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106
Communication dans un congrès inria-00525784v1
Image document

The Why/Krakatoa/Caduceus platform for deductive program verification

Jean-Christophe Filliâtre , Claude Marché
19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany
Communication dans un congrès inria-00270820v1
Image document

Separation Analysis for Weakest Precondition-based Verification

Thierry Hubert , Claude Marché
HAV 2007 - Heap Analysis and Verication, Mar 2007, Braga, Portugal. pp.81--93
Communication dans un congrès hal-03630177v1

Verification of Java Card applets behavior with respect to transactions and card tears

Claude Marché , Nicolas Rousset
Software Engineering and Formal Methods, Sep 2006, Pune, India
Communication dans un congrès inria-00129055v1
Image document

Reasoning about Java Programs with Aliasing and Frame Conditions

Claude Marché , Christine Paulin-Mohring
Theorem Proving in Higher Order Logics, 2005, Oxford, United Kingdom. pp.179-194, ⟨10.1007/11541868_12⟩
Communication dans un congrès hal-03274993v1
Image document

Formal proofs of numerical programs

Nguyen Thi Minh Tuyen , Sylvie Boldo , Claude Marché
Forum Digitéo, Oct 2010, Palaiseau, France
Poster de conférence inria-00536135v1

Formally Expressing what a Program Should Do: the ACSL Language

Allan Blanchard , Claude Marché , Virgile Prévosto
Nikolai Kosmatov; Julien Signoles. Guide to Software Verification with Frama-C - Core Components, Usages, and Applications, Springer, 2024
Chapitre d'ouvrage hal-04265707v1

Towards Modular Algebraic Specifications for Pointer Programs: a Case Study

Claude Marché
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
Chapitre d'ouvrage inria-00431399v1

Why3 version 1.0

Jean-Christophe Filliâtre , Andrei Paskevich , Guillaume Melquiond , Claude Marché , François Bobot
France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Brevet hal-03136256v1
Image document

A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions

Denis Cousineau , Hiroaki Inoue , Claude Marché , David Mentré
RT-0522, Inria. 2024
Rapport hal-04487766v1

ANSI/ISO C Specification Language Version 1.20

Patrick Baudin , Pascal Cuoq , Jean-Christophe Filliâtre , Claude Marché , Benjamin Monate
CEA List. 2024
Rapport hal-04523865v1
Image document

Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions

Paul Bonnot , Benoît Boyer , Florian Faissole , Claude Marché , Raphaël Rieu-Helft
RR-9531, Inria. 2023
Rapport hal-04343157v2
Image document

Formal Analysis of Ladder Programs using Deductive Verification

Cláudio Lourenço , Denis Cousineau , Florian Faissole , Claude Marché , David Mentré
[Research Report] RR-9402, Inria. 2021, pp.25
Rapport hal-03199464v1
Image document

Giant-step Semantics for the Categorisation of Counterexamples

Benedikt Becker , Cláudio Belo Lourenço , Claude Marché
[Research Report] RR-9407, Inria. 2021, pp.43
Rapport hal-03213438v1
Image document

The CREUSOT Environment for the Deductive Verification of Rust Programs

Xavier Denis , Jacques-Henri Jourdan , Claude Marché
[Research Report] RR-9448, Inria Saclay - Île de France. 2021
Rapport hal-03526634v2
Image document

Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup

Benedikt Becker , Jean-Christophe Filliâtre , Claude Marché
[Rapport Technique] Université Paris-Saclay. 2020
Rapport hal-02447409v1
Image document

Specification of UNIX Utilities

Nicolas Jeannerod , Claude Marché , Yann Régis-Gianas , Mihaela Sighireanu , Ralf Treinen
[Technical Report] ANR. 2019
Rapport hal-02321691v1
Image document

Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters

Benedikt Becker , Nicolas Jeannerod , Claude Marché , Ralf Treinen
[Technical Report] ANR. 2019
Rapport hal-02321743v1
Image document

Deductive Verification via Ghost Debugging

Martin Clochard , Andrei Paskevich , Claude Marché
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Rapport hal-01907894v1
Image document

Le langage CoLiS : syntaxe, sémantique et outillage

Ilham Dami , Claude Marché
[Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22
Rapport hal-01614488v1
Image document

Automated Verification of Floating-Point Computations in Ada Programs

Clément Fumex , Claude Marché , Yannick Moy
[Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53
Rapport hal-01511183v1
Image document

Counterexamples from proof failures in the SPARK program verifier

David Hauzar , Claude Marché , Yannick Moy
[Research Report] RR-8854, Inria. 2016, pp.22
Rapport hal-01271174v1
Image document

A Formal Proof of a Unix Path Resolution Algorithm

Ran Chen , Martin Clochard , Claude Marché
[Research Report] RR-8987, Inria. 2016, pp.27
Rapport hal-01406848v1
Image document

High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs

Claire Dross , Clément Fumex , Jens Gerlach , Claude Marché
[Research Report] RR-8821, Inria Saclay. 2015, pp.52
Rapport hal-01238376v1
Image document

Weakest Precondition Calculus, Revisited using Why3

Claude Marché , Asma Tafat
[Research Report] RR-8185, INRIA. 2012, pp.32
Rapport hal-00766171v1
Image document

Automated Generation of Loop Invariants using Predicate Abstraction

Krishnamani Kalyanasundaram , Claude Marché
[Research Report] RR-7714, INRIA. 2011, pp.32
Rapport inria-00615623v1
Image document

Binary Heaps Formally Verified in Why3

Asma Tafat , Claude Marché
[Research Report] RR-7780, INRIA. 2011, pp.33
Rapport inria-00636083v1
Image document

Proving Floating-Point Numerical Programs by Analysis of their Assembly Code

Nguyen Thi Minh Tuyen , Claude Marché
[Research Report] RR-7655, INRIA. 2011, pp.61
Rapport inria-00602266v1
Image document

A Certified Multi-prover Verification Condition Generator

Paolo Herms , Claude Marché , Benjamin Monate
[Research Report] RR-7793, INRIA. 2011, pp.22
Rapport hal-00639977v1
Image document

A Refinement Approach for Correct-by-Construction Object-Oriented Programs

Asma Tafat , Sylvain Boulmé , Claude Marché
[Research Report] RR-7310, INRIA. 2010, pp.31
Rapport inria-00491835v1
Image document

Regions and Permissions for Verifying Data Invariants

Romain Bardou , Claude Marché
[Research Report] RR-7412, INRIA. 2010, pp.40
Rapport inria-00525384v1
Image document

Modular Specification of Java Programs

Elena Tushkanova , Alain Giorgetti , Claude Marché , Olga Kouchnarenko
[Research Report] RR-7097, INRIA. 2009, pp.26
Rapport inria-00434452v1

Mechanically proving termination using polynomial interpretations

Evelyne Contejean , Claude Marché , Ana-Paula Tomas , Xavier Urbain
[Intern report] 1382, 2006
Rapport inria-00001167v1