2024
Conference papers
- titre
- De l'avantage de nuancer les décisions binaires
- auteur
- Claude Marché, Denis Cousineau
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
- titre
- Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function
- auteur
- Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
- article
- Formal Methods in Computer-Aided Design - FMCAD 2024, 2024, Prague, Czech Republic
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Formally Expressing what a Program Should Do: the ACSL Language
- auteur
- Allan Blanchard, Claude Marché, Virgile Prévosto
- article
- Nikolai Kosmatov; Julien Signoles. Guide to Software Verification with Frama-C - Core Components, Usages, and Applications, Springer, pp.3-80, 2024, ⟨10.1007/978-3-031-55608-1_1⟩
- Accès au bibtex
-
Reports
- titre
- A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions
- auteur
- Denis Cousineau, Hiroaki Inoue, Claude Marché, David Mentré
- article
- RT-0522, Inria. 2024
- Accès au texte intégral et bibtex
-
- titre
- ANSI/ISO C Specification Language Version 1.20
- auteur
- Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prévosto
- article
- CEA List. 2024
- Accès au bibtex
-
2023
Reports
- titre
- Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions
- auteur
- Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
- article
- RR-9531, Inria. 2023
- Accès au texte intégral et bibtex
-
2022
Journal articles
- titre
- The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages
- auteur
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- International Journal on Software Tools for Technology Transfer, 2022
- Accès au texte intégral et bibtex
-
- titre
- Automated Formal Analysis of Temporal Properties of Ladder Programs
- auteur
- Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Creusot: a Foundry for the Deductive Verification of Rust Programs
- auteur
- Xavier Denis, Jacques-Henri Jourdan, Claude Marché
- article
- ICFEM 2022 - 23th International Conference on Formal Engineering Methods, Oct 2022, Madrid, Spain
- Accès au texte intégral et bibtex
-
2021
Conference papers
- titre
- Automated Verification of Temporal Properties of Ladder Programs
- auteur
- Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
- Accès au texte intégral et bibtex
-
- titre
- Explaining Counterexamples with Giant-Step Assertion Checking
- auteur
- Benedikt Becker, Cláudio Belo Lourenço, Claude Marché
- article
- F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- The CREUSOT Environment for the Deductive Verification of Rust Programs
- auteur
- Xavier Denis, Jacques-Henri Jourdan, Claude Marché
- article
- [Research Report] RR-9448, Inria Saclay - Île de France. 2021
- Accès au texte intégral et bibtex
-
- titre
- Giant-step Semantics for the Categorisation of Counterexamples
- auteur
- Benedikt Becker, Cláudio Belo Lourenço, Claude Marché
- article
- [Research Report] RR-9407, Inria. 2021, pp.43
- Accès au texte intégral et bibtex
-
- titre
- Formal Analysis of Ladder Programs using Deductive Verification
- auteur
- Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- [Research Report] RR-9402, Inria. 2021, pp.25
- Accès au texte intégral et bibtex
-
2020
Conference papers
- titre
- Analysing installation scenarios of Debian packages
- auteur
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3
- auteur
- Diego Diverio, Cláudio Lourenço, Claude Marché
- article
- VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7
- Accès au texte intégral et bibtex
-
- titre
- Des transformations logiques passent leur certificat
- auteur
- Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich
- article
- JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
- Accès au texte intégral et bibtex
-
- titre
- Deductive Verification with Ghost Monitors
- auteur
- Martin Clochard, Claude Marché, Andrei Paskevich
- article
- POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup
- auteur
- Benedikt Becker, Jean-Christophe Filliâtre, Claude Marché
- article
- [Rapport Technique] Université Paris-Saclay. 2020
- Accès au texte intégral et bibtex
-
2019
Conference papers
- titre
- Ghost Code in Action: Automated Verification of a Symbolic Interpreter
- auteur
- Benedikt Becker, Claude Marché
- article
- 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⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- Specification of UNIX Utilities
- auteur
- Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
- article
- [Technical Report] ANR. 2019
- Accès au texte intégral et bibtex
-
- titre
- Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters
- auteur
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Ralf Treinen
- article
- [Technical Report] ANR. 2019
- Accès au texte intégral et bibtex
-
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
-
Conference papers
- titre
- Lightweight Interactive Proving inside an Automatic Program Verifier
- auteur
- Sylvain Dailler, Claude Marché, Yannick Moy
- article
- 4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
Patents
- titre
- Why3 version 1.0
- auteur
- Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot
- article
- France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
- Accès au 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
-
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
- 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
-
- 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
- Accès au texte intégral et 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. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- The CoLiS language: syntax, semantics and associated tools
- 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
-
- 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
-
- titre
- Let's Verify This with Why3
- auteur
- François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
- article
- International Journal on Software Tools for Technology Transfer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
- Accès au texte intégral et 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
-
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, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Formalizing Semantics with an Automatic Program Verifier
- auteur
- Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
- article
- 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
- Accès au texte intégral et 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
- Accès au texte intégral et 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. pp.290-293
- Accès au texte intégral et 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
- Accès au texte intégral et 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
- Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
- Accès au texte intégral et bibtex
-
- titre
- Calcul de plus faible précondition, revisité en Why3
- auteur
- Claude Marché, Asma Tafat
- article
- JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
- Accès au texte intégral et bibtex
-
Other publications
- titre
- The Why3 platform 0.81
- auteur
- François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
- article
- 2013
- Accès au texte intégral et 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
- ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy
- Accès au texte intégral et 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
-
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, 2011, 5, pp.377-393
- Accès au texte intégral et 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
- Accès au texte intégral et 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
- Accès au texte intégral et 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
- Accès au texte intégral et bibtex
-
Books
- 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é. Springer, 6528, pp.200, 2011
- Accès au 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
-
- 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
-
- 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
-
- 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
-
2010
Journal articles
- titre
- Modular inference of subprogram contracts for safety checking
- auteur
- Yannick Moy, Claude Marché
- article
- Journal of Symbolic Computation, 2010, 45, pp.1184-1211
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Multi-prover verification of floating-point programs
- auteur
- Ali Ayad, Claude Marché
- article
- Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- A refinement methodology for object-oriented programs
- auteur
- Asma Tafat, Sylvain Boulmé, Claude Marché
- article
- Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159
- Accès au texte intégral et 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
- Accès au texte intégral et bibtex
-
Books
- titre
- Formal Verification of Object-Oriented Software, Papers Presented at the International Conference
- auteur
- Bernhard Beckert, Claude Marché
- article
- Bernhard Beckert and Claude Marché. Karlsruhe University, 2010-13, pp.368, 2010, Karlsruhe Reports in Informatics
- Accès au 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
-
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
-
- 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
-
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
-
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, 2008, 21 (1-2), pp.59-88
- Accès au texte intégral et bibtex
-
2007
Conference papers
- titre
- The Why/Krakatoa/Caduceus platform for deductive program verification
- auteur
- Jean-Christophe Filliâtre, Claude Marché
- article
- 19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany
- Accès au texte intégral et bibtex
-
- titre
- Separation Analysis for Weakest Precondition-based Verification
- auteur
- Thierry Hubert, Claude Marché
- article
- HAV 2007 - Heap Analysis and Verication, Mar 2007, Braga, Portugal. pp.81--93
- Accès au texte intégral et 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
-
2006
Conference papers
- titre
- Verification of Java Card applets behavior with respect to transactions and card tears
- auteur
- Claude Marché, Nicolas Rousset
- article
- Software Engineering and Formal Methods, Sep 2006, Pune, India
- Accès au 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
-
2005
Journal articles
- titre
- Mechanically Proving Termination Using Polynomial Interpretations
- auteur
- Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain
- article
- Journal of Automated Reasoning, 2005, 34 (4), pp.325-363. ⟨10.1007/s10817-005-9022-x⟩
- Accès au bibtex
-
Conference papers
- titre
- Reasoning about Java Programs with Aliasing and Frame Conditions
- auteur
- Claude Marché, Christine Paulin-Mohring
- article
- Theorem Proving in Higher Order Logics, 2005, Oxford, United Kingdom. pp.179-194, ⟨10.1007/11541868_12⟩
- Accès au texte intégral et bibtex
-
2004
Journal articles
- titre
- Modular and Incremental Proofs of AC-Termination
- auteur
- Claude Marché, Xavier Urbain
- article
- Journal of Symbolic Computation, 2004, 38 (1), pp.873-897. ⟨10.1016/j.jsc.2004.02.003⟩
- Accès au bibtex
-
- titre
- The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML
- auteur
- Claude Marché, Christine Paulin-Mohring, Xavier Urbain
- article
- Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩
- Accès au bibtex
-