Publications HAL du projet ANR. proofinuse

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

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
titre
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
auteur
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery
article
2018
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01906155/file/paper.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
A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT
auteur
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex
article
29th International Conference on Computer Aided Verification, Jul 2017, Heidelberg, Germany. pp.419-435, ⟨10.1007/978-3-319-63390-9_22⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01522770/file/main.pdf BibTex
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

Reports

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

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