Publications : Claude Marché
You can find below a complete list of my publications, ordered by date of publication. You can also have a look at my publications on DBLP (conference papers and journals) and my publications on HAL (grouped by year of publication, and only for recent years).
Back| [150] | Allan Blanchard, Claude Marché, and Virgile Prevosto. Guide to Software Verification with Frama-C --- Core Components, Usages, and Applications, chapter Formally Expressing what a Program Should Do: the ACSL Language. Springer-Verlag, 2024. [ bib | full text on HAL ] |
| [149] | Claude Marché and Denis Cousineau. De l'avantage de nuancer les décisions binaires. In 35es Journées Francophones des Langages Applicatifs, 2024. [ bib | full text on HAL ] |
| [148] | Denis Cousineau, Hiroaki Inoue, Claude Marché, and David Mentré. A methodological guide for the validation of logic modelling of Ladder instructions. Technical Report 0522, Inria, 2024. [ bib | full text on HAL ] |
| [147] | Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and Raphaël Rieu-Helft. Formally verified bounds on rounding errors in concrete implementations of logarithm-sum-exponential functions. Research Report 9531, Inria, 2023. [ bib | full text on HAL ] |
| [146] |
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude
Marché, David Mentré, and Hiroaki Inoue.
Automated formal analysis of temporal properties of Ladder
programs.
International Journal on Software Tools for Technology
Transfer, 24(6):977--997, 2022.
[ bib |
DOI |
full text on HAL ]
Keywords: Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment |
| [145] |
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché.
Creusot: a foundry for the deductive verication of Rust programs.
In International Conference on Formal Engineering Methods -
ICFEM, Lecture Notes in Computer Science, Madrid, Spain, 2022. Springer.
[ bib |
full text on HAL ]
Keywords: Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits |
| [144] | Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. The CoLiS platform for the analysis of maintainer scripts in Debian software packages. International Journal on Software Tools for Technology Transfer, 2022. [ bib | full text on HAL ] |
| [143] | Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Explaining counterexamples with giant-step assertion checking. In José Creissac Campos and Andrei Paskevich, editors, 6th Workshop on Formal Integrated Development Environments (F-IDE 2021), Electronic Proceedings in Theoretical Computer Science, May 2021. [ bib | DOI | full text on HAL ] |
| [142] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Formal analysis of Ladder programs using deductive verification. Research Report RR-9402, Inria, April 2021. [ bib | full text on HAL ] |
| [141] | Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Giant-step semantics for the categorisation of counterexamples. Research Report RR-9407, Inria, April 2021. [ bib | full text on HAL ] |
| [140] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated verification of temporal properties of Ladder programs. In Formal Methods for Industrial Critical Systems, volume 12863 of Lecture Notes in Computer Science, pages 21--38, 2021. [ bib | DOI | full text on HAL ] |
| [139] | Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. The Creusot environment for the deductive verification of Rust programs. Research Report 9448, Inria Saclay - Île de France, 2021. [ bib | full text on HAL ] |
| [138] | Diego Diverio, Cláudio Belo Lourenço, and Claude Marché. “You-Know-Why”: an early-stage prototype of a key server developed using Why3. In VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event, pages 4--7, Dublin, Ireland, April 2020. Karlsruhe Institute of Technology. [ bib | DOI | full text on HAL ] |
| [137] | Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.16, 2020. [ bib | .html ] |
| [136] | Martin Clochard, Claude Marché, and Andrei Paskevich. Deductive verification with ghost monitors. In Principles of Programming Languages, New Orleans, United States, 2020. [ bib | DOI | full text on HAL ] |
| [135] | Quentin Garchery, Chantal Keller, Claude Marché, and Andrei Paskevich. Des transformations logiques passent leur certicat. In Zaynah Dargaye and Yann Régis-Gianas, editors, Trente-et-unièmes Journées Francophones des Langages Applicatifs, Gruissan, France, January 2020. [ bib | full text on HAL ] |
| [134] | Benedikt Becker, Jean-Christophe Filliâtre, and Claude Marché. Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup. Technical report, Université Paris-Saclay, January 2020. [ bib | full text on HAL ] |
| [133] | Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. Analysing installation scenarios of Debian packages. In Tools and Algorithms for the Construction and Analysis of Systems, volume 12079 of Lecture Notes in Computer Science, pages 235--253, 2020. [ bib | DOI | full text on HAL ] |
| [132] | Nicolas Jeannerod, Yann Régis-Gianas, Claude Marché, Mihaela Sighireanu, and Ralf Treinen. Specification of UNIX utilities. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ] |
| [131] | Benedikt Becker, Claude Marché, Nicolas Jeannerod, and Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ] |
| [130] | Benedikt Becker and Claude Marché. Ghost code in action: Automated verification of a symbolic interpreter. In Supratik Chakraborty and Jorge A.Navas, editors, Verified Software: Tools, Techniques and Experiments, volume 12031 of Lecture Notes in Computer Science, New York, United States, July 2019. [ bib | DOI | full text on HAL ] |
| [129] |
Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy.
Instrumenting a weakest precondition calculus for counterexample
generation.
Journal of Logical and Algebraic Methods in Programming,
99:97--113, 2018.
[ bib |
DOI |
full text on HAL ]
Keywords: Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples |
| [128] | Sylvain Dailler, Claude Marché, and Yannick Moy. Lightweight interactive proving inside an automatic program verifier. In Proceedings of the Fourth Workshop on Formal Integrated Development Environment, F-IDE, Oxford, UK, July 14, 2018, 2018. [ bib | DOI | full text on HAL ] |
| [127] | Martin Clochard, Andrei Paskevich, and Claude Marché. Deductive verification via ghost debugging. Research Report 9219, Inria, 2018. [ bib | full text on HAL ] |
| [126] | Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
| [125] | Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
| [124] | Ilham Dami and Claude Marché. The CoLiS language: syntax, semantics and associated tools. Technical Report 0491, Inria, October 2017. [ bib | full text on HAL ] |
| [123] |
Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond.
How to get an efficient yet verified arbitrary-precision integer
library.
In 9th Working Conference on Verified Software: Theories, Tools,
and Experiments, volume 10712 of Lecture Notes in Computer Science,
pages 84--101, Heidelberg, Germany, July 2017.
[ bib |
DOI |
full text on HAL |
.pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier |
| [122] | Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ] |
| [121] | Ran Chen, Martin Clochard, and Claude Marché. A formally proved, complete algorithm for path resolution with symbolic links. Journal of Formalized Reasoning, 10(1):51--66, 2017. [ bib | DOI | full text on HAL | http ] |
| [120] | Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016. [ bib | full text on HAL ] |
| [119] | Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 9952 of Lecture Notes in Computer Science, pages 461--478, Corfu, Greece, October 2016. Springer. [ bib | DOI | full text on HAL ] |
| [118] | Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché. Specification and proof of high-level functional properties of bit-level programs. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, pages 291--306, Minneapolis, MN, USA, June 2016. Springer. [ bib | full text on HAL ] |
| [117] | David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria Saclay Ile-de-France, February 2016. [ bib | full text on HAL ] |
| [116] | David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Rocco De Nicola and Eva Kühn, editors, Software Engineering and Formal Methods, Lecture Notes in Computer Science, pages 215--233, Vienna, Austria, 2016. [ bib | DOI | full text on HAL ] |
| [115] | Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib | full text on HAL ] |
| [114] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.org/download/manual-0.86.1.pdf. [ bib | .pdf ] |
| [113] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709--727, 2015. See also http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html. [ bib | DOI | full text on HAL ] |
| [112] | Claude Marché and Johannes Kanig. Bridging the gap between testing and formal verification in Ada development. ERCIM News, 100:38--39, January 2015. [ bib | full text on HAL ] |
| [111] |
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Formalizing semantics with an automatic program verifier.
In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th
Working Conference on Verified Software: Theories, Tools and Experiments
(VSTTE), volume 8471 of Lecture Notes in Computer Science, pages
37--51, Vienna, Austria, July 2014. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [110] |
David Delahaye, Claude Marché, and David Mentré.
Le projet BWare : une plate-forme pour la vérification
automatique d'obligations de preuve B.
In Approches Formelles dans l'Assistance au Développement de
Logiciels (AFADL), Paris, France, June 2014. EasyChair.
[ bib |
full text on HAL ]
Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financé pour 4 ans par le programme Ingénierie Numérique & Sécurité (INS) de l'Agence Nationale de la Recherche (ANR) et a débuté en septembre 2012 (voir le site web du projet : http://bware.lri.fr). Le consortium du projet BWare associe les partenaires académiques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R&D Centre Europe (MERCE), ClearSy, et OCamlPro
|
| [109] |
David Delahaye, Catherine Dubois, Claude Marché, and David Mentré.
The BWare project: Building a proof platform for the automated
verification of B proof obligations.
In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume
8477 of Lecture Notes in Computer Science, pages 290--293, Toulouse,
France, June 2014. Springer.
[ bib |
full text on HAL ]
We introduce BWare, an industrial research project that aims to provide a mechanized framework to support the automated veri cation of proof obligations coming from the development of industrial applications using the B method and requiring high integrity. The methodology adopted consists in building a generic verification platform relying on di erent theorem provers, such as rst order provers and SMT (Satisfiability Modulo Theories) solvers. Beyond the multi-tool aspect of our methodology, the originality of this project also resides in the requirement for the veri cation tools to produce proof objects, which are to be checked independently. In this paper, we present some preliminary results of BWare, as well as some current major lines of work
|
| [108] |
Claude Marché.
Verification of the functional behavior of a floating-point program:
an industrial case study.
Science of Computer Programming, 96(3):279--296, March 2014.
[ bib |
DOI |
full text on HAL |
.pdf ]
We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving
|
| [107] | Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages meets Program Verification (PLPV). ACM Press, 2014. [ bib | full text on HAL ] |
| [106] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.org/download/manual-0.82.pdf. [ bib | .pdf ] |
| [105] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
Preserving user proofs across specification changes.
In Ernie Cohen and Andrey Rybalchenko, editors, Verified
Software: Theories, Tools, Experiments (5th International Conference VSTTE),
volume 8164 of Lecture Notes in Computer Science, pages 191--201,
Atherton, USA, May 2013. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [104] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.81.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition,
March 2013.
http://why3.org/download/manual-0.81.pdf.
[ bib |
full text on HAL |
.pdf ]
Keywords: Why3 |
| [103] | Claude Marché and Asma Tafat. Calcul de plus faible précondition, revisité en Why3. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ] |
| [102] | Claude Marché and Asma Tafat. Weakest precondition calculus, revisited using Why3. Research Report RR-8185, INRIA, December 2012. [ bib | full text on HAL | .pdf ] |
| [101] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.80.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.80 edition,
October 2012.
https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf.
[ bib |
.pdf ]
Keywords: Why3 |
| [100] | J.-C. Filliâtre, C. Marché, Y. Moy, and R. Bardou. Why version 2.30. APP Deposit, August 2012. IDDN.FR.001.350004.000.S.P.2012.000.10000. [ bib ] |
| [99] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.73.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition,
July 2012.
[ bib |
.pdf ]
Keywords: Why3 |
| [98] |
David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi
Asuka.
Discharging proof obligations from Atelier B using multiple
automated provers.
In Steve Reeves and Elvinia Riccobene, editors, ABZ'2012 - 3rd
International Conference on Abstract State Machines, Alloy, B and Z, volume
7316 of Lecture Notes in Computer Science, pages 238--251, Pisa, Italy,
June 2012. Springer.
http://hal.inria.fr/hal-00681781/en/.
[ bib |
full text on HAL ]
We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.
|
| [97] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.72.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition,
May 2012.
[ bib |
.pdf ]
Keywords: Why3 |
| [96] | Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 2--17, Philadelphia, USA, January 2012. Springer. [ bib | full text on HAL | .pdf ] |
| [95] | 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, and Mattias Ulbrich. The COST IC0701 verification competition 2011. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, volume 7421 of Lecture Notes in Computer Science. Springer, 2012. [ bib | full text on HAL | .pdf ] |
| [94] | Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science, pages 314--329. Springer, December 2011. [ bib | full text on HAL ] |
| [93] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
The Why3 platform, version 0.71.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.71 edition,
October 2011.
https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf.
[ bib ]
Keywords: Why3 |
| [92] |
Asma Tafat and Claude Marché.
Binary heaps formally verified in Why3.
Research Report 7780, INRIA, October 2011.
http://hal.inria.fr/inria-00636083/en/.
[ bib |
full text on HAL ]
Keywords: Why3 |
| [91] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie [90], pages 53--64. https://hal.inria.fr/hal-00790310. [ bib ] |
| [90] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Why3: Shepherd your herd of provers.
In Boogie 2011: First International Workshop on Intermediate
Verification Languages, pages 53--64, Wroclaw, Poland, August 2011.
https://hal.inria.fr/hal-00790310.
[ bib |
full text on HAL ]
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. Keywords: Why3 |
| [89] | Krishnamani Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. http://hal.inria.fr/inria-00615623/en/. [ bib | full text on HAL ] |
| [88] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition,
February 2011.
http://why3.org/.
[ bib ]
Keywords: Why3 |
| [87] | Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in Frama-C --- Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib | PDF | http ] |
| [86] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153--167. Springer, January 2011. [ bib | full text on HAL ] |
| [85] | Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ] |
| [84] | Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377--393, 2011. [ bib | DOI | full text on HAL ] |
| [83] | Thi Minh Tuyen Nguyen and Claude Marché. Proving floating-point numerical programs by analysis of their assembly code. Research Report 7655, INRIA, 2011. http://hal.inria.fr/inria-00602266/en/. [ bib | full text on HAL ] |
| [82] | Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. Research Report 7793, INRIA, 2011. http://hal.inria.fr/hal-00639977/en/. [ bib | full text on HAL ] |
| [81] | Thi Minh Tuyen Nguyen, Sylvie Boldo, and Claude Marché. Formal proofs of numerical programs. Poster at the Digiteo Forum, Palaiseau, France, October 2010. [ bib | full text on HAL ] |
| [80] | Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 127--141, Edinburgh, Scotland, July 2010. Springer. [ bib | full text on HAL ] |
| [79] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pages 143--159, Paris, France, June 2010. http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083. [ bib | full text on HAL ] |
| [78] | Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ] |
| [77] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement approach for correct-by-construction object-oriented programs. Technical Report 7310, INRIA, 2010. [ bib | full text on HAL ] |
| [76] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. Submitted, 2010. [ bib | http ] |
| [75] | Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Specifying generic Java programs: two case studies. In PreProceedings of LDTA'2010, pages 92--106, 2010. http://ldta.info/preproceedings2010.pdf. [ bib ] |
| [74] | Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Specifying generic Java programs: two case studies. In Claus Brabrand and Pierre-Etienne Moreau, editors, Tenth Workshop on Language Descriptions, Tools and Applications. ACM Press, 2010. [ bib | full text on HAL ] |
| [73] | Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184--1211, 2010. [ bib | DOI | full text on HAL ] |
| [72] | Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Research Report 7412, INRIA, 2010. http://hal.inria.fr/inria-00525384/en/. [ bib | full text on HAL ] |
| [71] | Jean-Christophe Filliâtre and Claude Marché. Bibtex2html. APP Deposit, 2010. [ bib ] |
| [70] | Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ] |
| [69] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
| [68] |
Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko.
Modular specification of Java programs.
Technical Report 7097, INRIA, 2009.
[ bib |
full text on HAL ]
This work investigates the question of modular specification of generic Java classes and methods. The first part introduces a specification language for Java programs. In the second part the language is used to specify an array sorting algorithm by selection. The third and the fourth parts define a syntax proposal for the specification a generic Java programs, through two examples. The former is the specification of the generic method for sorting arrays which comes in the java.util.Arrays class of the Java API. The latter is the specification of the java.util.HashMap class and its use for memoization.
|
| [67] | Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf. [ bib | .pdf ] |
| [66] | Romain Bardou and Claude Marché. Regions and permissions for data invariants. Submitted, 2009. [ bib | http ] |
| [65] | Claude Marché. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification, Viinistu, Estonia, January 2009. http://krakatoa.lri.fr/ws/. [ bib | PDF | http ] |
| [64] | Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1--2):59--88, 2008. [ bib | full text on HAL | PDF | .pdf ] |
| [63] | Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ] |
| [62] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
| [61] | Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, 19th International Conference on Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 173--177, Berlin, Germany, July 2007. Springer. [ bib | DOI | full text on HAL | PDF ] |
| [60] | Claude Marché and Hans Zantema. The termination competition. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications (RTA'07), volume 4533 of Lecture Notes in Computer Science, pages 303--313, Paris, France, June 2007. Springer. [ bib | Slides | PDF | .pdf ] |
| [59] | Claude Marché, Hans Zantema, and Johannes Waldmann. The termination competition 2007. In Dieter Hofbauer and Alexander Serebrenik, editors, Extended Abstracts of the 9th International Workshop on Termination, WST'07, June 2007. http://www.lri.fr/~marche/termination-competition/. [ bib | http ] |
| [58] | Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), pages 81--93, Braga, Portugal, March 2007. [ bib | full text on HAL ] |
| [57] | Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), pages 35--51, Braga, Portugal, March 2007. [ bib | PDF | .pdf ] |
| [56] | Thierry Hubert and Claude Marché. Separation analysis for deductive verification. Technical report, Université Paris XI, 2007. http://www.lri.fr/~marche/separation.pdf. [ bib | PDF | .pdf ] |
| [55] | Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235--258. Springer, 2007. [ bib ] |
| [54] | Claude Marché. Jessie: an intermediate language for Java and C verification. In Programming Languages meets Program Verification (PLPV), pages 1--2, Freiburg, Germany, 2007. ACM Press. [ bib | DOI ] |
| [53] | Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. IEEE Comp. Soc. Press. [ bib ] |
| [52] | Claude Marché and Hans Zantema. The termination competition 2006. In Alfons Geser and Harald Sondergaard, editors, Extended Abstracts of the 8th International Workshop on Termination, WST'06, August 2006. http://www.lri.fr/~marche/termination-competition/. [ bib | http ] |
| [51] | Claude Marché. Preuves mécanisées de propriétés de programmes. Mémoire d'habilitation, Université Paris-Sud, December 2005. [ bib ] |
| [50] | Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ] |
| [49] | Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ] |
| [48] | Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179--194. Springer, August 2005. [ bib | .ps ] |
| [47] | Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Research Report DSIC II/01/05, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2005. [ bib ] |
| [46] | Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325--363, 2005. [ bib | DOI | Abstract ] |
| [45] | Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. 2005. [ bib | .ps ] |
| [44] |
Salvador Lucas, Claude Marché, and José Meseguer.
Operational termination of conditional term rewriting systems.
Information Processing Letters, 95:446--453, 2005.
[ bib ]
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs
|
| [43] | Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ] |
| [42] | Bart Jacobs, Claude Marché, and Nicole Rauch. Formal verification of a commercial smart card applet with multiple tools. In Algebraic Methodology and Software Technology, volume 3116 of Lecture Notes in Computer Science, Stirling, UK, July 2004. Springer. [ bib ] |
| [41] | Jean-Christophe Filliâtre and Claude Marché. Multi-Prover Verification of C Programs. In Sixth International Conference on Formal Engineering Methods, pages 15--29. Springer, 2004. [ bib | .ps.gz ] |
| [40] | Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ] |
| [39] | Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15--29, Seattle, WA, USA, November 2004. Springer. [ bib | .ps.gz ] |
| [38] | Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873--897, 2004. [ bib | http ] |
| [37] | Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ] |
| [36] | Claude Marché and Christine Paulin-Mohring. Reasoning on Java programs with aliasing and frame conditions. http://krakatoa.lri.fr/, 2004. [ bib ] |
| [35] | Néstor Cataño, Marek Gawkowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard Project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ] |
| [34] | Jean-Christophe Filliâtre, Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2003. http://krakatoa.lri.fr/. [ bib ] |
| [33] | Évelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. Proving termination of rewriting with cime. In Albert Rubio, editor, Extended Abstracts of the 6th International Workshop on Termination, WST'03, pages 71--73, June 2003. Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain. [ bib | http ] |
| [32] | Enno Ohlebusch, Claus Claves, and Claude Marché. The talp tool for termination analysis of logic programs. In Albert Rubio, editor, Extended Abstracts of the 6th International Workshop on Termination, WST'03, June 2003. http://bibiserv.techfak.uni-bielefeld.de/talp/. [ bib | http ] |
| [31] | Néstor Cataño, M. Gawlowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard project, 2003. [ bib ] |
| [30] | Keiichirou Kusakari, Claude Marché, and Xavier Urbain. Termination of associative-commutative rewriting using dependency pairs criteria. Research Report 1304, LRI, 2002. http://www.lri.fr/~urbain/textes/rr1304.ps.gz. [ bib | .ps.gz ] |
| [29] | Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2002. http://krakatoa.lri.fr/. [ bib ] |
| [28] | Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ] |
| [27] | Enno Ohlebusch, Claus Claves, and Claude Marché. TALP: A tool for the termination analysis of logic programs. In Leo Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 270--273, Norwich, UK, July 2000. Springer. Available at http://bibiserv.techfak.uni-bielefeld.de/talp/. [ bib | http ] |
| [26] | Évelyne Contejean, Claude Marché, Ana-Paola Tomás, and Xavier Urbain. Solving termination constraints via finite domain polynomial interpretations. Unpublished draft, International Workshop on Constraints in Computational Logics, Gif-sur-Yvette, France, September 1999. [ bib ] |
| [25] | Claude Marché. Normalized Rewriting: an unified view of Knuth-Bendix completion and Gröbner bases computation. Progress in Computer Science and Applied Logic, 15:193--208, 1998. [ bib | PDF | Abstract ] |
| [24] | Claude Marché and Xavier Urbain. Termination of associative-commutative rewriting by dependency pairs. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 241--255, Tsukuba, Japan, April 1998. Springer. [ bib | PDF | Abstract ] |
| [23] | Évelyne Contejean, Claude Marché, and Landy Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. Research report, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, 1997. [ bib ] |
| [22] | Évelyne Contejean, Claude Marché, and Landy Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In Hubert Comon, editor, 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 98--112, Barcelona, Spain, June 1997. Springer. [ bib | DOI | PDF | Abstract ] |
| [21] | Alexandre Boudet, Évelyne Contejean, and Claude Marché. AC Complete Unification and its Application to Theorem Proving. UNIF'96, June 1996. [ bib ] |
| [20] | Alexandre Boudet, Évelyne Contejean, and Claude Marché. AC-complete unification and its application to theorem proving. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 18--32, New Brunswick, NJ, USA, July 1996. Springer. [ bib | DOI | PDF | Abstract ] |
| [19] | Évelyne Contejean and Claude Marché. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416--419, New Brunswick, NJ, USA, July 1996. Springer. System Description available at http://cime.lri.fr/. [ bib | DOI | PDF | http | Abstract ] |
| [18] | Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253--288, 1996. [ bib | PDF | Abstract ] |
| [17] | Claude Marché. Associative-commutative reduction orderings via head-preserving interpretations. Technical Report 95--2, LIFAC, E.N.S. de Cachan, January 1995. [ bib | PDF | Abstract ] |
| [16] | Claude Marché. Normalized rewriting -- application to ground completion and standard bases. In Hubert Comon and Jean-Pierre Jouannaud, editors, Term Rewriting, volume 909 of Lecture Notes in Computer Science, pages 154--169. French Spring School of Theoretical Computer Science, Springer, 1995. [ bib | PDF | Abstract ] |
| [15] | Claude Marché. Normalized Rewriting: an unified view of Knuth-Bendix completion and Gröbner bases computation. In Manuel Bronstein and Volker Weispfenning, editors, Proceedings of the Conference on Symbolic Rewriting Techniques, Monte Verita, Switzerland, 1995. [ bib | PDF | Abstract ] |
| [14] | Claude Marché. Normalised rewriting and normalised completion. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 394--403, Paris, France, July 1994. IEEE Comp. Soc. Press. [ bib | PDF | Abstract ] |
| [13] | Claude Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories équationnelles. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 1993. [ bib | PDF | Abstract ] |
| [12] | Claude Marché. Normalized rewriting -- application to ground completion and standard bases. Notes de cours de l'école de printemps, 1993. [ bib | PDF | Abstract ] |
| [11] | Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104:29--51, 1992. [ bib | PDF | Abstract ] |
| [10] | Claude Marché. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81--92, 1992. [ bib | PDF | Abstract ] |
| [9] | Claude Marché. The word problem of ACD-ground theories is undecidable. Research Report 663, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, April 1991. [ bib ] |
| [8] | Claude Marché. On ground AC-completion. In Ronald. V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, April 1991. Springer. [ bib ] |
| [7] | Claude Marché. On AC-termination and ground AC-completion. Research Report 598, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, October 1990. [ bib ] |
| [6] | Jean-Pierre Jouannaud and Claude Marché. Completion modulo associativity, commutativity and identity. In Alfonso Miola, editor, Proc. Int. Symposium on Design and Implementation of Symbolic Computation Systems, LNCS 429, pages 111--120, Capri, Italy, April 1990. Springer. [ bib ] |
| [5] | Claude Marché. Complétion modulo associativité, commutativité et élément neutre. Research Report 513, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, September 1989. [ bib ] |
| [4] | Francisco Duran, Salvador Lucas, Claude Marché, José Meseguer, and Xavier Urbain. Termination of membership equational programs. Submitted. [ bib ] |
| [3] | Jean-Christophe Filliâtre, Thierry Hubert, and Claude Marché. The Caduceus tool for the verification of C programs. http://caduceus.lri.fr/. [ bib ] |
| [2] | Jean-Christophe Filliâtre and Claude Marché. Ocamlweb, a literate programming tool for Objective Caml. https://github.com/backtracking/ocamlweb/. [ bib | http ] |
| [1] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
http://why3.org/.
[ bib ]
Keywords: Why3 |
Back
This page was generated by bibtex2html.