 |
 |
 |
 |
|
|
|
|---|---|---|
|
inria-00525384v1
Rapport
Romain Bardou, Claude Marché. Regions and Permissions for Verifying Data Invariants [Research Report] RR-7412, INRIA. 2010, pp.40 |
||
|
hal-00772508v1
Communication dans un congrès
Thi Minh Tuyen Nguyen, Claude Marché. Hardware-Dependent Proofs of Numerical Programs Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011 |
||
|
hal-00772519v1
Direction d'ouvrage, Proceedings
Bernhard Beckert, Claude Marché. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010 Bernhard Beckert and Claude Marché. 6528, Springer, pp.200, 2011 |
||
|
inria-00534336v1
Communication dans un congrès
Asma Tafat, Sylvain Boulmé, Claude Marché. A refinement methodology for object-oriented programs 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; Formal Verification of Object-Oriented Software, Papers Presented at the International Conference |
||
|
hal-01067197v1
Communication dans un congrès
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier 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 |
||
|
hal-01314885v1
Communication dans un congrès
David Hauzar, Claude Marché, Yannick Moy. Counterexamples from Proof Failures in SPARK Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. Springer, 2016, Software Engineering and Formal Methods |
||
|
hal-01314876v1
Communication dans un congrès
Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché. Specification and Proof of High-Level Functional Properties of Bit-Level Programs NASA Formal methods, Jun 2016, Minneapolis, United States. Springer, 2016, NASA Formal methods |
||
|
inria-00270820v1
Communication dans un congrès
Jean-Christophe Filliâtre, Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification Werner Damm and Holger Hermanns. 19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany. 2007, Lecture Notes in Computer Science |
||
|
hal-00681781v1
Communication dans un congrès
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka. Discharging Proof Obligations from Atelier B using Multiple Automated Provers Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012 |
||
|
hal-01238376v1
Rapport
Claire Dross, Clément Fumex, Jens Gerlach, Claude Marché. High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs [Research Report] RR-8821, Inria Saclay. 2015, pp.52 |
||
|
hal-01102242v1
Article dans une revue
Claude Marché, Johannes Kanig. Bridging the Gap between Testing and Formal Verification in Ada Development ERCIM News, ERCIM, 2015, 100, pp.2. <http://ercim-news.ercim.eu/> |
||
|
inria-00602266v1
Rapport
Nguyen Thi Minh Tuyen, Claude Marché. Proving Floating-Point Numerical Programs by Analysis of their Assembly Code [Research Report] RR-7655, INRIA. 2011, pp.61 |
||
|
hal-00639977v1
Rapport
Paolo Herms, Claude Marché, Benjamin Monate. A Certified Multi-prover Verification Condition Generator [Research Report] RR-7793, INRIA. 2011, pp.22 |
||
|
hal-01534747v1
Communication dans un congrès
Nicolas Jeannerod, Claude Marché, Ralf Treinen. A Formally Verified Interpreter for a Shell-like Programming Language VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany |
||
|
hal-01534533v1
Communication dans un congrès
Clément Fumex, Claude Marché, Yannick Moy. Automating the Verification of Floating-Point Programs Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 9th Working Conference on Verified Software: Theories, Tools and Experiments. <http://vstte17.lri.fr/> |
||
|
hal-01511183v1
Rapport
Clément Fumex, Claude Marché, Yannick Moy. Automated Verification of Floating-Point Computations in Ada Programs [Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53 |
||
|
hal-01519732v1
Pré-publication, Document de travail
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library 2017 |
||
|
hal-00913431v1
Communication dans un congrès
Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014 |
||
|
inria-00001167v1
Rapport
Évelyne Contejean, Claude Marché, Ana-Paula Tomas, Xavier Urbain. Mechanically proving termination using polynomial interpretations [Intern report] 1382, 2006 |
||
|
hal-00790310v1
Communication dans un congrès
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Why3: Shepherd Your Herd of Provers Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64, 2011 |
||
|
hal-00998092v1
Communication dans un congrès
David Delahaye, Catherine Dubois, Claude Marché, David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science |
||
|
hal-00998094v1
Communication dans un congrès
David Delahaye, Claude Marché, David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France. EasyChair, 2014 |
||
|
inria-00536135v1
Poster
Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché. Formal proofs of numerical programs Forum Digitéo, Oct 2010, Palaiseau, France |
||
|
hal-01271174v1
Rapport
David Hauzar, Claude Marché, Yannick Moy. Counterexamples from proof failures in the SPARK program verifier [Research Report] RR-8854, Inria. 2016, pp.22 |
||
|
hal-00822856v1
Autre publication
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81 Tutorial and Reference Manual. 2013 |
||
|
hal-01344110v1
Communication dans un congrès
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. Springer, pp.16, 2016, 7th International Symposium on Leveraging Applications |
||
|
hal-00967132v1
Article dans une revue
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3 Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727 |
||
|
inria-00534339v1
Direction d'ouvrage, Proceedings
Bernhard Beckert, Claude Marché. Formal Verification of Object-Oriented Software, Papers Presented at the International Conference Bernhard Beckert and Claude Marché. 2010-13, Karlsruhe University, pp.368, 2010, Karlsruhe Reports in Informatics |
||
|
inria-00534333v1
Communication dans un congrès
Ali Ayad, Claude Marché. Multi-prover verification of floating-point programs 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 |
||
|
inria-00491835v1
Rapport
Asma Tafat, Sylvain Boulmé, Claude Marché. A Refinement Approach for Correct-by-Construction Object-Oriented Programs [Research Report] RR-7310, INRIA. 2010, pp.31 |
||
|
|
|