Skip to Main content Skip to Navigation

inria-00534339v1  Directions of work or proceedings
Bernhard BeckertClaude 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
hal-02355602v2  Conference papers
Benedikt BeckerNicolas JeannerodClaude MarchéYann Régis-GianasMihaela Sighireanu et al.  Analysing installation scenarios of Debian packages
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⟩
hal-03217393v1  Conference papers
Benedikt BeckerCláudio LourençoClaude Marché. Explaining Counterexamples with Giant-Step Assertion Checking
F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩
hal-00967132v1  Journal articles
François BobotJean-Christophe FilliâtreClaude MarchéAndrei Paskevich. Let's Verify This with Why3
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
hal-03281580v1  Conference papers
Cláudio LourençoDenis CousineauFlorian FaissoleClaude MarchéDavid Mentré et al.  Automated Verification of Temporal Properties of Ladder Programs
FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
hal-00875395v1  Conference papers
François BobotJean-Christophe FilliâtreClaude MarchéGuillaume MelquiondAndrei Paskevich. Preserving User Proofs Across Specification Changes
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
hal-01344110v1  Conference papers
Nikolai KosmatovClaude MarchéYannick MoyJulien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478
inria-00534331v1  Journal articles
Yannick MoyClaude Marché. Modular inference of subprogram contracts for safety checking
Journal of Symbolic Computation, Elsevier, 2010, 45, pp.1184-1211
hal-00998092v1  Conference papers
David DelahayeCatherine DuboisClaude 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. pp.290-293
hal-00998094v1  Conference papers
David DelahayeClaude 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
hal-01534533v1  Conference papers
Clément FumexClaude MarchéYannick Moy. Automating the Verification of Floating-Point Programs
9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany
hal-01614488v1  Reports
Ilham DamiClaude Marché. Le langage CoLiS : syntaxe, sémantique et outillage
[Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22
hal-00789525v1  Conference papers
Thorsten BormerMarc BrockschmidtDino DistefanoGidon ErnstJean-Christophe Filliâtre et al.  The COST IC0701 Verification Competition 2011
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy
hal-01067197v1  Conference papers
Martin ClochardJean-Christophe FilliâtreClaude MarchéAndrei Paskevich. Formalizing Semantics with an Automatic Program Verifier
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
inria-00431474v1  Journal articles
Francisco DuránSalvador LucasClaude MarchéJosé MeseguerXavier Urbain. Proving Operational Termination of Membership Equational Programs
Higher-Order and Symbolic Computation, Springer Verlag, 2008, 21 (1-2), pp.59-88
hal-00681781v1  Conference papers
David MentréClaude MarchéJean-Christophe FilliâtreMasashi Asuka. Discharging Proof Obligations from Atelier B using Multiple Automated Provers
ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy
hal-01534747v1  Conference papers
Nicolas JeannerodClaude 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-03136256v1  Patents
Jean-Christophe FilliâtreAndrei PaskevichGuillaume MelquiondClaude MarchéFrançois Bobot. Why3 version 1.0
France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
hal-00913431v1  Conference papers
Martin ClochardClaude MarchéAndrei Paskevich. Verified Programs with Binders
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
hal-02276257v1  Conference papers
Benedikt BeckerClaude Marché. Ghost Code in Action: Automated Verification of a Symbolic Interpreter
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⟩