Publications HAL

2024

Conference papers

titre
De l'avantage de nuancer les décisions binaires
auteur
Claude Marché, Denis Cousineau
article
JFLA 2024 – 35es Journées Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04342273/file/jfla2024-paper-33.pdf BibTex

Book sections

titre
Formally Expressing what a Program Should Do: the ACSL Language
auteur
Allan Blanchard, Claude Marché, Virgile Prévosto
article
Nikolai Kosmatov; Julien Signoles. Guide to Software Verification with Frama-C - Core Components, Usages, and Applications, Springer, 2024
Accès au bibtex
BibTex

Reports

titre
A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions
auteur
Denis Cousineau, Hiroaki Inoue, Claude Marché, David Mentré
article
RT-0522, Inria. 2024
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04487766/file/RT-0522.pdf BibTex
titre
ANSI/ISO C Specification Language Version 1.20
auteur
Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prévosto
article
CEA List. 2024
Accès au bibtex
BibTex

2023

Reports

titre
Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions
auteur
Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
article
RR-9531, Inria. 2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04343157/file/RR-9531v2.pdf BibTex

2022

Journal articles

titre
The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages
auteur
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
article
International Journal on Software Tools for Technology Transfer, 2022
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03737886/file/main.pdf BibTex
titre
Automated Formal Analysis of Temporal Properties of Ladder Programs
auteur
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
article
International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03737869/file/sttt.pdf BibTex

Conference papers

titre
Creusot: a Foundry for the Deductive Verification of Rust Programs
auteur
Xavier Denis, Jacques-Henri Jourdan, Claude Marché
article
ICFEM 2022 - 23th International Conference on Formal Engineering Methods, Oct 2022, Madrid, Spain
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03737878/file/main.pdf BibTex

2021

Conference papers

titre
Automated Verification of Temporal Properties of Ladder Programs
auteur
Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
article
FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03281580/file/main.pdf BibTex
titre
Explaining Counterexamples with Giant-Step Assertion Checking
auteur
Benedikt Becker, Cláudio Belo Lourenço, Claude Marché
article
F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03217393/file/fide.pdf BibTex

Reports

titre
The CREUSOT Environment for the Deductive Verification of Rust Programs
auteur
Xavier Denis, Jacques-Henri Jourdan, Claude Marché
article
[Research Report] RR-9448, Inria Saclay - Île de France. 2021
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03526634/file/report.pdf BibTex
titre
Giant-step Semantics for the Categorisation of Counterexamples
auteur
Benedikt Becker, Cláudio Belo Lourenço, Claude Marché
article
[Research Report] RR-9407, Inria. 2021, pp.43
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03213438/file/RR-9407.pdf BibTex
titre
Formal Analysis of Ladder Programs using Deductive Verification
auteur
Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
article
[Research Report] RR-9402, Inria. 2021, pp.25
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03199464/file/RR-9402.pdf BibTex

2020

Conference papers

titre
Analysing installation scenarios of Debian packages
auteur
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
article
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⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02355602/file/main.pdf BibTex
titre
You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3
auteur
Diego Diverio, Cláudio Lourenço, Claude Marché
article
VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03002187/file/main.pdf BibTex
titre
Des transformations logiques passent leur certificat
auteur
Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich
article
JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02384946/file/main.pdf BibTex
titre
Deductive Verification with Ghost Monitors
auteur
Martin Clochard, Claude Marché, Andrei Paskevich
article
POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02368284/file/article.pdf BibTex

Reports

titre
Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup
auteur
Benedikt Becker, Jean-Christophe Filliâtre, Claude Marché
article
[Rapport Technique] Université Paris-Saclay. 2020
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02447409/file/main.pdf BibTex

2019

Conference papers

titre
Ghost Code in Action: Automated Verification of a Symbolic Interpreter
auteur
Benedikt Becker, Claude Marché
article
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⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02276257/file/Ghost_Code_in_Action_Automated_Verification_of_a_Symbolic_Interpreter.pdf BibTex

Reports

titre
Specification of UNIX Utilities
auteur
Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
article
[Technical Report] ANR. 2019
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02321691/file/main.pdf BibTex
titre
Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters
auteur
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Ralf Treinen
article
[Technical Report] ANR. 2019
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02321743/file/main.pdf BibTex

2018

Journal articles

titre
Instrumenting a Weakest Precondition Calculus for Counterexample Generation
auteur
Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy
article
Journal of Logical and Algebraic Methods in Programming, 2018, 99, pp.97-113
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01802488/file/jlamp.pdf BibTex

Conference papers

titre
Lightweight Interactive Proving inside an Automatic Program Verifier
auteur
Sylvain Dailler, Claude Marché, Yannick Moy
article
4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01936302/file/article.pdf BibTex

Patents

titre
Why3 version 1.0
auteur
Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot
article
France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Accès au bibtex
BibTex

Reports

titre
Deductive Verification via Ghost Debugging
auteur
Martin Clochard, Andrei Paskevich, Claude Marché
article
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01907894/file/RR-9219.pdf BibTex

Preprints, Working Papers, ...

titre
Deductive Verification with Ghost Monitors
auteur
Martin Clochard, Claude Marché, Andrei Paskevich
article
2018
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01926659/file/article.pdf BibTex

2017

Journal articles

titre
A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links
auteur
Ran Chen, Martin Clochard, Claude Marché
article
Journal of Formalized Reasoning, 2017, 10 (1)
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01652148/file/jfr7213.pdf BibTex

Conference papers

titre
Automating the Verification of Floating-Point Programs
auteur
Clément Fumex, Claude Marché, Yannick Moy
article
9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01534533/file/article.pdf BibTex
titre
A Formally Verified Interpreter for a Shell-like Programming Language
auteur
Nicolas Jeannerod, Claude Marché, Ralf Treinen
article
VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany
Accès au texte intégral et bibtex
https://hal.science/hal-01534747/file/jeannerod-marche-treinen-vstte17.pdf BibTex
titre
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
auteur
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
article
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⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01519732/file/main.pdf BibTex

Reports

titre
Le langage CoLiS : syntaxe, sémantique et outillage
auteur
Ilham Dami, Claude Marché
article
[Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01614488/file/RT-0491.pdf BibTex
titre
Automated Verification of Floating-Point Computations in Ada Programs
auteur
Clément Fumex, Claude Marché, Yannick Moy
article
[Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01511183/file/RR-9060.pdf BibTex

2016

Conference papers

titre
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014
auteur
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
article
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01344110/file/paper063.pdf BibTex
titre
Counterexamples from Proof Failures in SPARK
auteur
David Hauzar, Claude Marché, Yannick Moy
article
Software Engineering and Formal Methods, Jul 2016, Vienna, Austria
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01314885/file/article.pdf BibTex
titre
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
auteur
Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché
article
NASA Formal methods, Jun 2016, Minneapolis, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01314876/file/article-final.pdf BibTex

Reports

titre
A Formal Proof of a Unix Path Resolution Algorithm
auteur
Ran Chen, Martin Clochard, Claude Marché
article
[Research Report] RR-8987, Inria. 2016, pp.27
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01406848/file/RR-8987.pdf BibTex
titre
Counterexamples from proof failures in the SPARK program verifier
auteur
David Hauzar, Claude Marché, Yannick Moy
article
[Research Report] RR-8854, Inria. 2016, pp.22
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01271174/file/RR-8854.pdf BibTex

2015

Journal articles

titre
Bridging the Gap between Testing and Formal Verification in Ada Development
auteur
Claude Marché, Johannes Kanig
article
ERCIM News, 2015, 100, pp.2
Accès au bibtex
BibTex
titre
Let's Verify This with Why3
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
International Journal on Software Tools for Technology Transfer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00967132/file/main.pdf BibTex

Reports

titre
High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs
auteur
Claire Dross, Clément Fumex, Jens Gerlach, Claude Marché
article
[Research Report] RR-8821, Inria Saclay. 2015, pp.52
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01238376/file/RR-8821.pdf BibTex

2014

Journal articles

titre
Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study
auteur
Claude Marché
article
Science of Computer Programming, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00967124/file/main.pdf BibTex

Conference papers

titre
Formalizing Semantics with an Automatic Program Verifier
auteur
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01067197/file/main.pdf BibTex
titre
Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B
auteur
David Delahaye, Claude Marché, David Mentré
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00998094/file/afadl2014_submission_6.pdf BibTex
titre
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
auteur
David Delahaye, Catherine Dubois, Claude Marché, David Mentré
article
Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00998092/file/bware_ABZ_14_.pdf BibTex
titre
Verified Programs with Binders
auteur
Martin Clochard, Claude Marché, Andrei Paskevich
article
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00913431/file/plpv03-clochard.pdf BibTex

2013

Conference papers

titre
Preserving User Proofs Across Specification Changes
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
article
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00875395/file/main.pdf BibTex
titre
Calcul de plus faible précondition, revisité en Why3
auteur
Claude Marché, Asma Tafat
article
JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00778791/file/jfla2013-01.pdf BibTex

Other publications

titre
The Why3 platform 0.81
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
article
2013
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00822856/file/manual-0.81.pdf BibTex

2012

Conference papers

titre
Discharging Proof Obligations from Atelier B using Multiple Automated Provers
auteur
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
article
ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00681781/file/main.pdf BibTex

Reports

titre
Weakest Precondition Calculus, Revisited using Why3
auteur
Claude Marché, Asma Tafat
article
[Research Report] RR-8185, INRIA. 2012, pp.32
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00766171/file/RR-8185.pdf BibTex

2011

Journal articles

titre
Formal verification of numerical programs: from C annotated programs to mechanical proofs
auteur
Sylvie Boldo, Claude Marché
article
Mathematics in Computer Science, 2011, 5, pp.377-393
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00777605/file/boldo11mcs.pdf BibTex

Conference papers

titre
Hardware-Dependent Proofs of Numerical Programs
auteur
Thi Minh Tuyen Nguyen, Claude Marché
article
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00772508/file/main.pdf BibTex
titre
Why3: Shepherd Your Herd of Provers
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00790310/file/main.pdf BibTex
titre
The COST IC0701 Verification Competition 2011
auteur
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
article
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00789525/file/costcomp2011.pdf BibTex

Books

titre
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010
auteur
Bernhard Beckert, Claude Marché
article
Bernhard Beckert and Claude Marché. Springer, 6528, pp.200, 2011
Accès au bibtex
BibTex

Reports

titre
A Certified Multi-prover Verification Condition Generator
auteur
Paolo Herms, Claude Marché, Benjamin Monate
article
[Research Report] RR-7793, INRIA. 2011, pp.22
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00639977/file/RR-7793.pdf BibTex
titre
Binary Heaps Formally Verified in Why3
auteur
Asma Tafat, Claude Marché
article
[Research Report] RR-7780, INRIA. 2011, pp.33
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00636083/file/main.pdf BibTex
titre
Automated Generation of Loop Invariants using Predicate Abstraction
auteur
Krishnamani Kalyanasundaram, Claude Marché
article
[Research Report] RR-7714, INRIA. 2011, pp.32
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00615623/file/main.pdf BibTex
titre
Proving Floating-Point Numerical Programs by Analysis of their Assembly Code
auteur
Nguyen Thi Minh Tuyen, Claude Marché
article
[Research Report] RR-7655, INRIA. 2011, pp.61
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00602266/file/main.pdf BibTex

2010

Journal articles

titre
Modular inference of subprogram contracts for safety checking
auteur
Yannick Moy, Claude Marché
article
Journal of Symbolic Computation, 2010, 45, pp.1184-1211
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00534331/file/YJSCO1169.pdf BibTex

Conference papers

titre
Multi-prover verification of floating-point programs
auteur
Ali Ayad, Claude Marché
article
Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00534333/file/main.pdf BibTex
titre
A refinement methodology for object-oriented programs
auteur
Asma Tafat, Sylvain Boulmé, Claude Marché
article
Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00534336/file/13.pdf BibTex
titre
Specifying Generic Java Programs: two case studies
auteur
Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko
article
11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00525784/file/gmtkLDTA2010.pdf BibTex

Books

titre
Formal Verification of Object-Oriented Software, Papers Presented at the International Conference
auteur
Bernhard Beckert, Claude Marché
article
Bernhard Beckert and Claude Marché. Karlsruhe University, 2010-13, pp.368, 2010, Karlsruhe Reports in Informatics
Accès au bibtex
BibTex

Poster communications

titre
Formal proofs of numerical programs
auteur
Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché
article
Forum Digitéo, Oct 2010, Palaiseau, France
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00536135/file/posterDIGITEO.pdf BibTex

Reports

titre
Regions and Permissions for Verifying Data Invariants
auteur
Romain Bardou, Claude Marché
article
[Research Report] RR-7412, INRIA. 2010, pp.40
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00525384/file/RR-7412.pdf BibTex
titre
A Refinement Approach for Correct-by-Construction Object-Oriented Programs
auteur
Asma Tafat, Sylvain Boulmé, Claude Marché
article
[Research Report] RR-7310, INRIA. 2010, pp.31
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00491835/file/RR-7310.pdf BibTex

2009

Reports

titre
Modular Specification of Java Programs
auteur
Elena Tushkanova, Alain Giorgetti, Claude Marché, Olga Kouchnarenko
article
[Research Report] RR-7097, INRIA. 2009, pp.26
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00434452/file/RR-7097.pdf BibTex

2008

Journal articles

titre
Proving Operational Termination of Membership Equational Programs
auteur
Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain
article
Higher-Order and Symbolic Computation, 2008, 21 (1-2), pp.59-88
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00431474/file/duran08hosc.pdf BibTex

2007

Conference papers

titre
The Why/Krakatoa/Caduceus platform for deductive program verification
auteur
Jean-Christophe Filliâtre, Claude Marché
article
19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00270820/file/cav.pdf BibTex
titre
Separation Analysis for Weakest Precondition-based Verification
auteur
Thierry Hubert, Claude Marché
article
HAV 2007 - Heap Analysis and Verication, Mar 2007, Braga, Portugal. pp.81--93
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03630177/file/hubert07hav.pdf BibTex

Book sections

titre
Towards Modular Algebraic Specifications for Pointer Programs: a Case Study
auteur
Claude Marché
article
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
Accès au bibtex
BibTex

2006

Conference papers

titre
Verification of Java Card applets behavior with respect to transactions and card tears
auteur
Claude Marché, Nicolas Rousset
article
Software Engineering and Formal Methods, Sep 2006, Pune, India
Accès au bibtex
BibTex

Reports

titre
Mechanically proving termination using polynomial interpretations
auteur
Evelyne Contejean, Claude Marché, Ana-Paula Tomas, Xavier Urbain
article
[Intern report] 1382, 2006
Accès au bibtex
BibTex

2005

Journal articles

titre
Mechanically Proving Termination Using Polynomial Interpretations
auteur
Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain
article
Journal of Automated Reasoning, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩
Accès au bibtex
BibTex

Conference papers

titre
Reasoning about Java Programs with Aliasing and Frame Conditions
auteur
Claude Marché, Christine Paulin-Mohring
article
Theorem Proving in Higher Order Logics, 2005, Oxford, United Kingdom. pp.179-194, ⟨10.1007/11541868_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03274993/file/marche05tphols.pdf BibTex

2004

Journal articles

titre
Modular and Incremental Proofs of AC-Termination
auteur
Claude Marché, Xavier Urbain
article
Journal of Symbolic Computation, 2004, 38 (1), pp.873-897. ⟨10.1016/j.jsc.2004.02.003⟩
Accès au bibtex
BibTex
titre
The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML
auteur
Claude Marché, Christine Paulin-Mohring, Xavier Urbain
article
Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩
Accès au bibtex
BibTex