Publications HAL

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, ASDD-AlmaDL, 2017, 10 (1)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652148/file/jfr7213.pdf BibTex

Conference papers

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. 10712, 2017, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01534747/file/jeannerod-marche-treinen-vstte17.pdf BibTex
titre
Automating the Verification of Floating-Point Programs
auteur
Clément Fumex, Claude Marché, Yannick Moy
article
Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 10712, 2017, Lecture Notes in Computer Science. 〈http://vstte17.lri.fr/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01534533/file/article.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. 10712, 2017, Lecture Notes in Computer Science. 〈https://vstte17.lri.fr/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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. Springer, pp.16, 2016, 7th International Symposium on Leveraging Applications
Accès au texte intégral et bibtex
https://hal.inria.fr/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. Springer, 2016, Software Engineering and Formal Methods
Accès au texte intégral et bibtex
https://hal.inria.fr/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. Springer, 2016, NASA Formal methods
Accès au texte intégral et bibtex
https://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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, ERCIM, 2015, 100, pp.2. 〈http://ercim-news.ercim.eu/〉
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
Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727
Accès au texte intégral et bibtex
https://hal.inria.fr/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://hal.inria.fr/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, Elsevier, 2014, 93 (3), pp.279-296. 〈10.1016/j.scico.2014.04.003〉
Accès au texte intégral et bibtex
https://hal.inria.fr/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
Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/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. EasyChair, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/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. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/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. ACM Press, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/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
Ernie Cohen and Andrey Rybalchenko. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. Springer, 8164, pp.191-201, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00875395/file/main.pdf BibTex
titre
Calcul de plus faible précondition, revisité en Why3
auteur
Claude Marché, Asma Tafat
article
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/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
Tutorial and Reference Manual. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/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
Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/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://hal.inria.fr/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, Springer, 2011, 5, pp.377-393
Accès au texte intégral et bibtex
https://hal.inria.fr/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. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772508/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. Springer, 7421, 2012, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00789525/file/costcomp2011.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, 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00790310/file/main.pdf BibTex

Directions of work or proceedings

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é. 6528, Springer, 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://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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, Elsevier, 2010, 45, pp.1184-1211
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534331/file/YJSCO1169.pdf BibTex

Conference papers

titre
Multi-prover verification of floating-point programs
auteur
Ali Ayad, Claude Marché
article
Jürgen Giesl and Reiner Hähnle. Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6173, 2010, Lecture Notes in Artificial Intelligence
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534333/file/main.pdf BibTex
titre
A refinement methodology for object-oriented programs
auteur
Asma Tafat, Sylvain Boulmé, Claude Marché
article
Bernhard Beckert and Claude Marché. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. Karlsruhe University, 2010-13, pp.143--159, 2010, Karlsruhe Reports in Informatics
Accès au texte intégral et bibtex
https://hal.inria.fr/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, 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00525784/file/gmtkLDTA2010.pdf BibTex

Directions of work or proceedings

titre
Formal Verification of Object-Oriented Software, Papers Presented at the International Conference
auteur
Bernhard Beckert, Claude Marché
article
Bernhard Beckert and Claude Marché. 2010-13, Karlsruhe University, 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://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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://hal.inria.fr/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, Springer Verlag, 2008, 21 (1-2), pp.59-88
Accès au texte intégral et bibtex
https://hal.inria.fr/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
Werner Damm and Holger Hermanns. 19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany. 2007, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00270820/file/cav.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
Dang Van Hung, Paritosh Pandya. Software Engineering and Formal Methods, Sep 2006, Pune, India. IEEE Comp. Soc. Press, 2006, th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)
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