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
-
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
-
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
-
- 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
-
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
-
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
-
- 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
-
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
-
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
-
- 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
-
- 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
-
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
-
- 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
-
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
-
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
-