Publications : JeanChristophe Filliâtre
Back[136]  JeanChristophe Filliâtre and Andrei Paskevich. L'arithmétique de séparation. In Timothy Bourke and Delphine Demange, editors, JFLA 2023  34èmes Journées Francophones des Langages Applicatifs, pages 274283, 2023. [ bib  full text on HAL ] 
[135]  JeanChristophe Filliâtre and Clément Pascutto. Optimizing prestate copies in runtime verification of function postconditions. In 22nd International Conference on Runtime Verification, 2022. [ bib  full text on HAL ] 
[134]  Thibaut Balabonski, Sylvain Conchon, JeanChristophe Filliâtre, Kim Nguyen, and Laurent Sartre. Informatique  MP2I/MPI  CPGE 1re et 2e années  Cours et exercices corrigés. Ellipses, 2022. [ bib  full text on HAL ] 
[133]  JeanChristophe Filliâtre. Compterendu de fin de projet anr15ce250008 “vocal”. Technical report, Laboratoire Méthodes Formelles, June 2021. [ bib  full text on HAL ] 
[132] 
JeanChristophe Filliâtre and Clément Pascutto.
Ortac: Runtime assertion checking for OCaml.
In Proceedings of the 21st International Conference on Runtime
Verification (RV'21), May 2021.
[ bib 
full text on HAL ]
Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime. In this work, we present ortac, a runtime assertion checking tool for OCaml libraries and programs. OCaml is a functional programming lan guage in which idioms rely on an expressive type system, modules, and interface abstractions. ortac consumes interfaces annotated with type invariants and function contracts and produces code wrappers with the same signature that check these specifications at runtime. It provides a flexible framework for traditional assertion checking, monitoring mis behaviors without interruptions, and automated fuzz testing for OCaml programs. This paper presents an overview of ortac features and highlights its main design choices.

[131]  JeanChristophe Filliâtre. Simpler proofs with decentralized invariants. Journal of Logical and Algebraic Methods in Programming, 121, January 2021. See http://why3.lri.fr/spdi/. [ bib  DOI  full text on HAL ] 
[130]  JeanChristophe Filliâtre and Clément Pascutto. Ortac: Runtime assertion checking for OCaml. In 21st International Conference on Runtime Verification, 2021. [ bib  full text on HAL ] 
[129]  JeanChristophe Filliâtre and Andrei Paskevich. Solution to verifythis 2021 challenge 2, 2021. https://toccata.gitlabpages.inria.fr/toccata/gallery/verifythis_2021_dll_to_bst.en.html. [ bib ] 
[128]  JeanChristophe Filliâtre and Andrei Paskevich. Abstraction and genericity in Why3. In Tiziana Margaria and Bernhard Steffen, editors, 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 12476 of Lecture Notes in Computer Science, pages 122142, Rhodes, Greece, October 2020. Springer. See also http://why3.lri.fr/isola2020/. [ bib  full text on HAL ] 
[127]  JeanChristophe Filliâtre. A Coq retrospective  at the heart of Coq architecture, the genesis of version 7.0. In The Coq Workshop 2020, virtual, July 2020. Invited talk. [ bib  full text on HAL  http ] 
[126]  Patrick Baudin, Pascal Cuoq, JeanChristophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.16, 2020. [ bib  .html ] 
[125]  JeanChristophe Filliâtre. Mesurer la hauteur d'un arbre. In Zaynah Dargaye and Yann RégisGianas, editors, Trenteetunièmes Journées Francophones des Langages Applicatifs, Gruissan, France, January 2020. https://www.lri.fr/~filliatr/hauteur/. [ bib  full text on HAL  Slides ] 
[124]  Benedikt Becker, JeanChristophe Filliâtre, and Claude Marché. Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup. Technical report, Université ParisSaclay, January 2020. [ bib  full text on HAL ] 
[123]  Thibaut Balabonski, Sylvain Conchon, JeanChristophe Filliâtre, and Kim Nguyen. Numérique et Sciences Informatiques, 24 leçons avec exercices corrigés. Terminale. Ellipses, 2020. [ bib  full text on HAL ] 
[122]  JeanChristophe Filliâtre. Deductive verification of OCaml libraries. In 15th International Conference on integrated Formal Methods, Bergen, Norway, December 2019. Invited talk. [ bib  full text on HAL ] 
[121]  Arthur Charguéraud, JeanChristophe Filliâtre, Cláudio Belo Lourenço, and Mário Pereira. GOSPEL  providing OCaml with a formal specification language. In Annabelle McIver and Maurice ter Beek, editors, FM 2019 23rd International Symposium on Formal Methods, Porto, Portugal, October 2019. [ bib  full text on HAL ] 
[120]  Thibaut Balabonski, Sylvain Conchon, JeanChristophe Filliâtre, and Kim Nguyen. Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Ellipses, August 2019. [ bib  http ] 
[119]  JeanChristophe Filliâtre. The Why3 tool for deductive verification and verified OCaml libraries. In FramaC & SPARK Day 2019, Paris, France, June 2019. Invited talk. [ bib ] 
[118]  JeanChristophe Filliâtre. Retour sur 25 ans de programmation avec OCaml. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. Séminaire invité. [ bib  full text on HAL ] 
[117]  JeanChristophe Filliâtre. Parcours d'un informaticien. Séminaire Info Pour Tous, September 2018. Séminaire invité. [ bib  http ] 
[116]  JeanChristophe Filliâtre. An introduction to deductive program verification. Mathematical Summer in Paris (summer school), July 2018. Cours invité. [ bib ] 
[115]  JeanChristophe Filliâtre. Autoactive verification using Why3's IDE. In 4th Workshop on Formal Integrated Development Environment, Oxford, UK, July 2018. Invited talk. [ bib ] 
[114]  JeanChristophe Filliâtre, Mário Pereira, and Simão Melo de Sousa. Vérification de programmes fortement impératifs avec Why3. In Sylvie Boldo and Nicolas Magaud, editors, Vingtneuvièmes Journées Francophones des Langages Applicatifs, Banyulssurmer, France, January 2018. [ bib  full text on HAL  .pdf ] 
[113]  JeanChristophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, and Simão Melo de Sousa. A toolchain to Produce CorrectbyConstruction OCaml Programs. Technical report, 2018. artifact: https://www.lri.fr/~mpereira/correct_ocaml.ova. [ bib  full text on HAL  .pdf ] 
[112]  JeanChristophe Filliâtre. Deductive program verification. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving  9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 912, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science. Springer, 2018. Invited talk. [ bib ] 
[111]  JeanChristophe Filliâtre. Why3  where programs meet provers. In KeY Symposium 2017, Rastatt, Germany, October 2017. Invited talk. [ bib ] 
[110]  Arthur Charguéraud, JeanChristophe Filliâtre, Mário Pereira, and François Pottier. VOCAL  A Verified OCaml Library. ML Family Workshop, September 2017. [ bib  full text on HAL ] 
[109]  JeanChristophe Filliâtre. Vérification déductive de programmes. Séminaire Acquérir une culture commune dans le domaine de l'informatique, lycée Diderot, Paris, May 2017. Séminaire invité. [ bib ] 
[108]  JeanChristophe Filliâtre. Why3 tutorial. In VerifyThis 2017, Uppsala, Sweden, April 2017. Invited tutorial. [ bib ] 
[107]  JeanChristophe Filliâtre and Mário Pereira. Producing all ideals of a forest, formally (verification pearl). In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib  full text on HAL ] 
[106] 
JeanChristophe Filliâtre and Mário Pereira.
A modular way to reason about iteration.
In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA
Formal Methods Symposium, volume 9690 of Lecture Notes in Computer
Science, Minneapolis, MN, USA, June 2016. Springer.
[ bib 
full text on HAL ]
In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the nite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with nondeterministic and possibly innite iteration. We show how to cope with the issue of an iteration no longer being consistent with mutable data. We validate our proposal using the deductive verication tool Why3 and two iteration paradigms, namely cursors and higherorder iterators. For each paradigm, we verify several implementations of iterators and client code. This is done in a modular way, i.e., the client code only relies on the specication of the iteration.

[105] 
JeanChristophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
The spirit of ghost code.
Formal Methods in System Design, 48(3):152174, 2016.
[ bib 
DOI 
full text on HAL ]
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many stateoftheart program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. Keywords: Why3 
[104]  JeanChristophe Filliâtre and Mário Pereira. Itérer avec confiance. In Vingtseptièmes Journées Francophones des Langages Applicatifs, SaintMalo, France, January 2016. [ bib  full text on HAL ] 
[103] 
JeanChristophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
A pragmatic type system for deductive verification.
Research report, Université Paris Sud, 2016.
https://hal.archivesouvertes.fr/hal01256434v3.
[ bib 
full text on HAL ]
In the context of deductive verication, it is customary today to handle programs with pointers using either separation logic, dynamic frames, or explicit memory models. Yet we can observe that in numerous programs, a large amount of code ts within the scope of Hoare logic, provided we can statically control aliasing. When this is the case, the code correctness can be reduced to simpler verication conditions which do not require any explicit memory model. This makes verication conditions more amenable both to automated theorem proving and to manual inspection and debugging. In this paper, we devise a method of such static aliasing control for a programming language featuring nested data structures with mutable components. Our solution is based on a type system with singleton regions and eects, which we prove to be sound.

[102] 
Martin Clochard, JeanChristophe Filliâtre, and Andrei Paskevich.
How to avoid proving the absence of integer overflows.
In Arie Gurfinkel and Sanjit A. Seshia, editors, 7th Working
Conference on Verified Software: Theories, Tools and Experiments (VSTTE),
volume 9593 of Lecture Notes in Computer Science, pages 94109, San
Francisco, California, USA, July 2015. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[101]  François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.lri.fr/download/manual0.86.1.pdf. [ bib  .pdf ] 
[100]  JeanChristophe Filliâtre. Vérification déductive de programmes. Mathematic Park, Institut Henri Poincaré, March 2015. Séminaire invité. [ bib  http ] 
[99]  François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709727, 2015. See also http://toccata.lri.fr/gallery/fm2012comp.en.html. [ bib  DOI  full text on HAL ] 
[98]  Sylvain Conchon and JeanChristophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, September 2014. [ bib  full text on HAL  http ] 
[97] 
JeanChristophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
The spirit of ghost code.
In Armin Biere and Roderick Bloem, editors, 26th International
Conference on Computer Aided Verification, volume 8859 of Lecture Notes
in Computer Science, pages 116, Vienna, Austria, July 2014. Springer.
[ bib 
full text on HAL 
.pdf ]
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many stateoftheart program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. Keywords: Why3 
[96] 
Martin Clochard, JeanChristophe 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
3751, Vienna, Austria, July 2014. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[95]  JeanChristophe Filliâtre. Démonstration. l'ordinateur à la rescousse. Tangente (horssérie numéro 52), (52):3436, February 2014. [ bib ] 
[94]  JeanChristophe Filliâtre. Deductive program verification with Why3. In Mathematical Structures of Computation  Formal Proof, Symbolic Computation and Computer Arithmetic, Lyon, France, February 2014. Invited talk. [ bib ] 
[93]  Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325352, 2014. [ bib  DOI  full text on HAL  http ] 
[92]  JeanChristophe Filliâtre. Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml. In Vingtcinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. https://www.lri.fr/~filliatr/publis/bouturage.pdf. [ bib ] 
[91]  François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.lri.fr/download/manual0.82.pdf. [ bib  .pdf ] 
[90]  Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco, Gilles Dowek, JeanChristophe Filliâtre, and Stéphane Gonnord. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Eyrolles, August 2013. [ bib  full text on HAL  http ] 
[89] 
JeanChristophe Filliâtre.
One logic to use them all.
In 24th International Conference on Automated Deduction
(CADE24), volume 7898 of Lecture Notes in Artificial Intelligence,
pages 120, Lake Placid, USA, June 2013. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[88] 
François Bobot, JeanChristophe 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 191201,
Atherton, USA, May 2013. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[87]  JeanChristophe Filliâtre. Deductive program verification with Why3. In MSRInria Joint Centre “Spring Day”, Lyon, France, May 2013. Invited talk. [ bib ] 
[86]  Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423456, April 2013. [ bib  DOI  full text on HAL ] 
[85] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.81.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.81 edition,
March 2013.
http://why3.lri.fr/download/manual0.81.pdf.
[ bib 
full text on HAL 
.pdf ]
Keywords: Why3 
[84]  JeanChristophe Filliâtre and Andrei Paskevich. Why3  where programs meet provers. In ESOP [83], pages 125128. [ bib ] 
[83] 
JeanChristophe Filliâtre and Andrei Paskevich.
Why3  where programs meet provers.
In Matthias Felleisen and Philippa Gardner, editors, Proceedings
of the 22nd European Symposium on Programming, volume 7792 of Lecture
Notes in Computer Science, pages 125128. Springer, March 2013.
[ bib 
full text on HAL ]
Keywords: Why3 
[82]  JeanChristophe Filliâtre and Rémy El Sibaïe. Combine : une bibliothèque OCaml pour la combinatoire. In Vingtquatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://www.lri.fr/~filliatr/combine/. [ bib  full text on HAL  .pdf ] 
[81]  JeanChristophe Filliâtre. Deductive Program Verification. In Nate Foster, Philippa Gardner, Alan Schmitt, Gareth Smith, Peter Thieman, and Tobias Wrigstad, editors, Programming Languages Mentoring Workshop (PLMW 2013), Rome, Italy, January 2013. [ bib  full text on HAL ] 
[80] 
JeanChristophe Filliâtre.
Deductive program verification with Why3.
Lecture notes for the First DigiCosme Spring School,
https://www.lri.fr/~marche/DigiCosmeSchool/filliatre.html, 2013.
[ bib ]
Keywords: Why3 
[79] 
François Bobot and JeanChristophe Filliâtre.
Separation predicates: a taste of separation logic in firstorder
logic.
In 14th International Conference on Formal Ingineering Methods
(ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto,
Japan, November 2012. Springer.
[ bib 
full text on HAL 
.pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional firstorder logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from userdefined inductive predicates. We illustrate this idea on a nontrivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers AltErgo, CVC3, and Z3.

[78] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.80.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.80 edition,
October 2012.
https://gforge.inria.fr/docman/view.php/2990/8186/manual0.80.pdf.
[ bib 
.pdf ]
Keywords: Why3 
[77]  José Bacelar Almeida, Manuel Barbosa, JeanChristophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. CAOVerif: An opensource deductive verification platform for cryptographic software implementations. Science of Computer Programming, October 2012. Accepted for publication. [ bib  DOI ] 
[76] 
Mário Pereira, JeanChristophe Filliâtre, and Simão Melo de Sousa.
ARMY: a deductive verification platform for ARM programs using
Why3.
In INForum 2012, September 2012.
[ bib 
.pdf ]
Unstructured (lowlevel) programs tend to be challenging to prove correct, since the control flow is arbitrary complex and there are no obvious points in the code where to insert logical assertions. In this paper, we present a system to formally verify ARM programs, based on a flow sequentialization methodology and a formalized ARM semantics. This system, built upon the why3 verification platform, takes an annotated ARM program, turns it into a set of purely sequential flow programs, translates these programs' instructions into the corresponding formalized opcodes and finally calls the Why3 VCGen to generate the verification conditions that can then be discharged by provers. A prototype has been implemented and used to verify several programming examples. Keywords: Why3 
[75]  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 ] 
[74] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.73.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.73 edition,
July 2012.
[ bib 
.pdf ]
Keywords: Why3 
[73]  JeanChristophe Filliâtre. Combining Interactive and Automated Theorem Proving using Why3 (invited tutorial). In Zvonimir Rakamarić, editor, Second International Workshop on Intermediate Verification Languages (BOOGIE 2012), Berkeley, California, USA, July 2012. [ bib ] 
[72] 
David Mentré, Claude Marché, JeanChristophe 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 238251, Pisa, Italy,
June 2012. Springer.
http://hal.inria.fr/hal00681781/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 firstorder logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.

[71] 
JeanChristophe Filliâtre, Andrei Paskevich, and Aaron Stump.
The 2nd verified software competition: Experience report.
In Vladimir Klebanov and Sarah Grebing, editors, COMPARE2012:
1st International Workshop on Comparative Empirical Evaluation of Reasoning
Systems, Manchester, UK, June 2012. EasyChair.
[ bib 
full text on HAL 
.pdf ]
We report on the second verified software competition. It was organized by the three authors on a 48 hours period on November 810, 2011. This paper describes the competition, presents the five problems that were proposed to the participants, and gives an overview of the solutions sent by the 29 teams that entered the competition.

[70] 
JeanChristophe Filliâtre.
Course notes EJCP 2012, chapter Vérification déductive de
programmes avec Why3.
June 2012.
[ bib 
http ]
Keywords: Why3 
[69] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.72.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.72 edition,
May 2012.
[ bib 
.pdf ]
Keywords: Why3 
[68]  JeanChristophe Filliâtre. Combining Interactive and Automated Theorem Proving in Why3 (invited talk). In Keijo Heljanko and Hugo Herbelin, editors, Automation in Proof Assistants 2012, Tallinn, Estonia, April 2012. [ bib ] 
[67] 
JeanChristophe Filliâtre.
Verifying two lines of C with Why3: an exercise in program
verification.
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 8397, Philadelphia, USA, January 2012. Springer.
[ bib 
.pdf ]
This article details the formal verification of a 2line C program that computes the number of solutions to the nqueens problem. The formal proof of (an abstraction of) the C code is performed using the Why3 tool to generate the verification conditions and several provers (AltErgo, CVC3, Coq) to discharge them. The main purpose of this article is to illustrate the use of Why3 in verifying an algorithmically complex program. Keywords: Why3 
[66]  Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, JeanChristophe 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 ObjectOriented 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 ] 
[65]  JeanChristophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université ParisSud, December 2011. [ bib  .pdf ] 
[64] 
Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
[ bib 
full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the onedimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floatingpoint computation leads to roundoff errors. We formally specify in Coq the numerical scheme, prove both the method error and the roundoff error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machinechecked. Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis 
[63]  JeanChristophe Filliâtre, Andrei Paskevich, and Aaron Stump. The 2nd Verified Software Competition, November 2011. https://sites.google.com/site/vstte2012/compet. [ bib ] 
[62] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei
Paskevich.
The Why3 platform, version 0.71.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.71 edition,
October 2011.
https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf.
[ bib ]
Keywords: Why3 
[61]  François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie [60], pages 5364. https://hal.inria.fr/hal00790310. [ bib ] 
[60] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Why3: Shepherd your herd of provers.
In Boogie 2011: First International Workshop on Intermediate
Verification Languages, pages 5364, Wroclaw, Poland, August 2011.
https://hal.inria.fr/hal00790310.
[ 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 
[59] 
JeanChristophe Filliâtre.
Deductive software verification.
International Journal on Software Tools for Technology Transfer
(STTT), 13(5):397403, August 2011.
[ bib 
DOI 
.pdf ]
Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. We briefly review this research area, with an emphasis on tools.

[58] 
Claire Dross, JeanChristophe Filliâtre, and Yannick Moy.
Correct Code Containing Containers.
In 5th International Conference on Tests and Proofs (TAP'11),
volume 6706 of Lecture Notes in Computer Science, pages 102118,
Zurich, June 2011. Springer.
[ bib 
full text on HAL 
.pdf ]
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to adhoc data structures based on pointers. As standards like DO178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and userprovided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.

[57] 
JeanChristophe Filliâtre and Krishnamani Kalyanasundaram.
Functory: A distributed computing library for Objective Caml.
In Trends in Functional Programming, volume 7193 of
Lecture Notes in Computer Science, pages 6581, Madrid, Spain, May 2011.
[ bib 
.pdf ]
We present Functory, a distributed computing library for Objective Caml. The main features of this library include (1) a polymorphic API, (2) several implementations to adapt to different deployment scenarios such as sequential, multicore or network, and (3) a reliable faulttolerance mechanism. This paper describes the motivation behind this work, as well as the design and implementation of the library. It also demonstrates the potential of the library using realistic experiments.

[56] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.64 edition,
February 2011.
http://why3.lri.fr/.
[ bib ]
Keywords: Why3 
[55]  JeanChristophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingtdeuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib  .pdf ] 
[54]  Manuel Barbosa, JeanChristophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. A deductive verification platform for cryptographic software. In 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33, Pisa, Italy, September 2010. Electronic Communications of the EASST. [ bib  http ] 
[53]  Sylvain Conchon, JeanChristophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation tempsréel de programmes Caml. In Vingtetunièmes Journées Francophones des Langages Applicatifs, VieuxPort La Ciotat, France, January 2010. INRIA. [ bib  .pdf ] 
[52]  Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal proof of a wave equation resolution scheme: the method error. In Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 147162. Springer, 2010. [ bib  DOI  full text on HAL ] 
[51]  JeanChristophe Filliâtre and Claude Marché. Bibtex2html. APP Deposit, 2010. [ bib ] 
[50] 
Johannes Kanig and JeanChristophe Filliâtre.
Who: A Verifier for Effectful Higherorder Programs.
In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August
2009.
[ bib 
full text on HAL 
.pdf ]
We present Who, a tool for verifying effectful higherorder functions. It features Effect polymorphism, higherorder logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is intended to be used as an intermediate language for verification tools targeting MLlike programming languages.

[49]  Sylvie Boldo, JeanChristophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying FloatingPoint Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 5974, Grand Bend, Canada, July 2009. Springer. [ bib  DOI ] 
[48]  JeanChristophe Filliâtre. Invited tutorial: Why  an intermediate language for deductive program verification. In Hassen Saïdi and Natarajan Shankar, editors, Automated Formal Methods (AFM09), Grenoble, France, 2009. [ bib ] 
[47]  Patrick Baudin, JeanChristophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://framac.cea.fr/acsl.html. [ bib  PDF  .html ] 
[46] 
Romain Bardou, JeanChristophe Filliâtre, Johannes Kanig, and Stéphane
Lescuyer.
Faire bonne figure avec Mlpost.
In Vingtièmes Journées Francophones des Langages
Applicatifs, SaintQuentin sur Isère, January 2009. INRIA.
[ bib 
.pdf ]
Cet article présente Mlpost, une bibliothèque Ocaml de dessin scientifique. Elle s'appuie sur Metapost, qui permet notamment d'inclure des fragments L^{A}T_{E}X dans les figures. Ocaml offre une alternative séduisante aux langages de macros L^{A}T_{E}X, aux langages spécialisés ou même aux outils graphiques. En particulier, l'utilisateur de Mlpost bénéficie de toute l'expressivité d'Ocaml et de son typage statique. Enfin Mlpost propose un style déclaratif qui diffère de celui, souvent impératif, des outils existants.

[45] 
JeanChristophe Filliâtre.
A Functional Implementation of the GarsiaWachs Algorithm.
In ACM SIGPLAN Workshop on ML, Victoria, British Columbia,
Canada, September 2008. ACM Press.
[ bib 
PDF 
.pdf ]
This functional pearl proposes an ML implementation of the GarsiaWachs algorithm. This somewhat obscure algorithm builds a binary tree with minimum weighted path length from weighted leaf nodes given in symmetric order. Our solution exhibits the usual benefits of functional programming (use of immutable data structures, patternmatching, polymorphism) and nicely compares to the purely imperative implementation from The Art of Computer Programming.

[44]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Marco T. Morazán, editor, Trends in Functional Programming Volume 8: Selected Papers of the 8^{th} International Symposium on Trends in Functional Programming (TFP'07), New York, USA, volume 8. Intellect, 2008. [ bib ] 
[43]  Sylvain Conchon and JeanChristophe Filliâtre. SemiPersistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib  PDF  .pdf ] 
[42] 
JeanChristophe Filliâtre.
Gagner en passant à la corde.
In Dixneuvièmes Journées Francophones des Langages
Applicatifs, Étretat, France, January 2008. INRIA.
[ bib 
PDF 
.pdf ]
Cet article présente une réalisation en Ocaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de données s'écrit naturellement comme un foncteur, transformant une structure de séquence en une autre structure de même interface. Cette fonctorisation a de nombreuses applications audelà de l'article original. Nous en donnons plusieurs, dont un éditeur de texte dont les performances sur de très gros fichiers sont bien meilleures que celles des éditeurs les plus populaires.

[41]  JeanChristophe Filliâtre. Using SMT solvers for deductive verification of C and Java programs. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, Princeton, USA, 2008. [ bib ] 
[40]  Patrick Baudin, JeanChristophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://framac.cea.fr/acsl.html. [ bib  PDF  .html ] 
[39] 
Sylvain Conchon and JeanChristophe Filliâtre.
A Persistent UnionFind Data Structure.
In ACM SIGPLAN Workshop on ML, pages 3745, Freiburg, Germany,
October 2007. ACM Press.
[ bib 
PDF 
.pdf ]
The problem of disjoint sets, also known as unionfind, consists in maintaining a partition of a finite set within a data structure. This structure provides two operations: a function find returning the class of an element and a function union merging two classes. An optimal and imperative solution is known since 1975. However, the imperative nature of this data structure may be a drawback when it is used in a backtracking algorithm. This paper details the implementation of a persistent unionfind data structure as efficient as its imperative counterpart. To achieve this result, our solution makes heavy use of imperative features and thus it is a significant example of a data structure whose side effects are safely hidden behind a persistent interface. To strengthen this last claim, we also detail a formalization using the Coq proof assistant which shows both the correctness of our solution and its observational persistence.

[38] 
JeanChristophe Filliâtre.
Formal Verification of MIX Programs.
In Journées en l'honneur de Donald E. Knuth, Bordeaux,
France, October 2007.
http://knuth07.labri.fr/exposes.php.
[ bib 
PDF 
.pdf ]
We introduce a methodology to formally verify MIX programs. It consists in annotating a MIX program with logical annotations and then to turn it into a set of purely sequential programs on which classical techniques can be applied. Contrary to other approaches of verification of unstructured programs, we do not impose the location of annotations but only the existence of at least one invariant on each cycle in the control flow graph. A prototype has been implemented and used to verify several programs from The Art of Computer Programming.

[37]  JeanChristophe 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 173177, Berlin, Germany, July 2007. Springer. [ bib  DOI  full text on HAL  PDF ] 
[36] 
Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles.
Designing a Generic Graph Library using ML Functors.
In Marco T. Morazán and Henrik Nilsson, editors, The Eighth
Symposium on Trends in Functional Programming, volume TRSHUCS2007041,
pages XII/113, New York, USA, April 2007. Seton Hall University.
[ bib 
.ps ]
This paper details the design and implementation of Ocamlgraph, a highly generic graph library for the programming language Ocaml. This library features a large set of graph data structuresdirected or undirected, with or without labels on vertices and edges, as persistent or mutable data structures, etc.and a large set of graph algorithms. Algorithms are written independently from graph data structures, which allows combining user data structure (resp. algorithm) with Ocamlgraph algorithm (resp. data structure). Genericity is obtained through massive use of the Ocaml module system and its functions, the socalled functors.

[35]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Trends in Functional Programming (TFP'07), New York City, USA, April 2007. [ bib  PDF  .pdf ] 
[34] 
Sylvie Boldo and JeanChristophe Filliâtre.
Formal verification of floatingpoint programs.
In 18th IEEE International Symposium on Computer Arithmetic,
pages 187194, 2007.
[ bib 
DOI 
PDF 
.pdf ]
This paper introduces a methodology to perform formal verification of floatingpoint C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floatingpoint arithmetic. The Caduceus firstorder logic model for C programs is extended accordingly. Then verification conditions expressing the correctness of the programs are obtained in the usual way and can be discharged interactively with the Coq proof assistant, using an existing Coq formalization of floatingpoint arithmetic. This methodology is already implemented and has been successfully applied to several short floatingpoint programs, which are presented in this paper.

[33] 
Sylvain Conchon and JeanChristophe Filliâtre.
UnionFind Persistant.
In Dixhuitièmes Journées Francophones des Langages
Applicatifs, pages 135149. INRIA, January 2007.
[ bib 
PDF 
.pdf ]
Le problème des classes disjointes, connu sous le nom de unionfind, consiste à maintenir dans une structure de données une partition d'un ensemble fini. Cette structure fournit deux opérations : une fonction find déterminant la classe d'un élément et une fonction union réunissant deux classes. Une solution optimale et impérative, due à Tarjan, est connue depuis longtemps.

[32]  JeanChristophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification, 2007. http://why.lri.fr/queens/. [ bib  PDF  http ] 
[31]  Sylvain Conchon and JeanChristophe Filliâtre. TypeSafe Modular HashConsing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib  PDF  .pdf ] 
[30]  JeanChristophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib  PDF  .pdf ] 
[29] 
Nicolas Ayache and JeanChristophe Filliâtre.
Combining the Coq proof assistant with firstorder decision
procedures.
http://www.lri.fr/~filliatr/publis/coqdp.ps.gz, March 2006.
[ bib 
.ps.gz ]
We present an integration of firstorder automatic theorem provers into the Coq proof assistant. This integration is based on a translation from the higherorder logic of Coq, the Calculus of Inductive Constructions, to a polymorphic firstorder logic. This translation is defined and proved sound in this paper. It includes not only the translation of terms and predicates belonging to the firstorder fragment, but also several techniques to go well beyond: abstractions of higherorder subterms, caseanalysis, mutually recursive functions and inductive types. This process has been implemented in the Coq proof assistant to call the decision procedures Simplify, CVC Lite, haRVey and Zenon through Coq tactics. The first experiments are promising.

[28]  JeanChristophe Filliâtre. Itérer avec persistance. In Dixseptièmes Journées Francophones des Langages Applicatifs. INRIA, January 2006. [ bib  .ps.gz ] 
[27]  JeanChristophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib  .ps.gz ] 
[26]  JeanChristophe Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332240, 2006. [ bib  DOI  PDF  .pdf ] 
[25]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 7994. INRIA, March 2005. [ bib  .ps.gz ] 
[24]  JeanChristophe Filliâtre and Pierre Letouzey. Functors for Proofs and Programs. In Proceedings of The European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 370384, Barcelona, Spain, April 2004. [ bib  PDF  .pdf ] 
[23]  JeanChristophe Filliâtre and Claude Marché. MultiProver Verification of C Programs. In Sixth International Conference on Formal Engineering Methods, pages 1529. Springer, 2004. [ bib  .ps.gz ] 
[22]  JeanChristophe Filliâtre and Claude Marché. Multiprover 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 1529, Seattle, WA, USA, November 2004. Springer. [ bib  .ps.gz ] 
[21]  JeanChristophe Filliâtre and F. Pottier. Producing All Ideals of a Forest, Functionally. Journal of Functional Programming, 13(5):945956, September 2003. [ bib  PDF ] 
[20]  JeanChristophe Filliâtre. Verification of nonfunctional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709745, July 2003. [ bib  PDF  .pdf ] 
[19]  JeanChristophe Filliâtre. Verification of nonfunctional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709745, July 2003. [ bib  .ps.gz ] 
[18]  JeanChristophe Filliâtre. Why: a multilanguage multiprover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. http://www.lri.fr/~filliatr/ftp/publis/whytool.ps.gz. [ bib  .ps.gz ] 
[17]  JeanChristophe Filliâtre, Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2003. http://krakatoa.lri.fr/. [ bib ] 
[16]  JeanChristophe Filliâtre. The Why verification tool, 2002. http://why.lri.fr/. [ bib  http ] 
[15]  JeanChristophe Filliâtre. La supériorité de l'ordre supérieur. In Journées Francophones des Langages Applicatifs, pages 1526, Anglet, France, January 2002. [ bib  PDF  .pdf ] 
[14]  JeanChristophe Filliâtre, Sam Owre, Harald Rueß, and Natarajan Shankar. ICS: Integrated Canonization and Solving (Tool presentation). In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV'2001, volume 2102 of Lecture Notes in Computer Science, pages 246249. Springer, 2001. [ bib ] 
[13]  JeanChristophe Filliâtre. Design of a proof assistant: Coq version 7. Research Report 1369, LRI, Université Paris Sud, October 2000. [ bib  full text on HAL  .ps.gz ] 
[12]  JeanChristophe Filliâtre. Hash consing in an ML framework. Research Report 1368, LRI, Université Paris Sud, September 2000. [ bib  .ps.gz ] 
[11]  JeanChristophe Filliâtre. A theory of monads parameterized by effects. Research Report 1367, LRI, Université Paris Sud, November 1999. [ bib  .ps.gz ] 
[10]  B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual  Version V6.3, July 1999. http://coq.inria.fr/doc/main.html. [ bib  Abstract ] 
[9]  JeanChristophe Filliâtre. Preuve de programmes impératifs en théorie des types. PhD thesis, Université ParisSud, July 1999. [ bib  .ps.gz ] 
[8]  JeanChristophe Filliâtre and Nicolas Magaud. Certification of Sorting Algorithms in the System Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, Nice, France, 1999. [ bib  .ps.gz ] 
[7]  B. Barras, S. Boutin, C. Cornes, J. Courant, D. Delahaye, D. de Rauglaudre, J.C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent, C. PaulinMohring, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.2. INRIARocquencourtCNRSUniversité Paris Sud ENS Lyon, May 1998. [ bib  ftp ] 
[6]  JeanChristophe Filliâtre. Proof of Imperative Programs in Type Theory. In Proceedings of the TYPES'98 workshop, volume 1657 of Lecture Notes in Computer Science. Springer, 1998. [ bib  .ps.gz ] 
[5]  JeanChristophe Filliâtre. Une procédure de décision pour le calcul des prédicats direct  etude et implémentation dans le système coq. Master's thesis, LIP (ENS Lyon), 1994. [ bib ] 
[4]  JeanChristophe Filliâtre, Thierry Hubert, and Claude Marché. The Caduceus tool for the verification of C programs. http://caduceus.lri.fr/. [ bib ] 
[3]  Sylvain Conchon and JeanChristophe Filliâtre. Semipersistent data structures. Technical report. [ bib ] 
[2]  JeanChristophe Filliâtre and Claude Marché. Ocamlweb, a literate programming tool for Objective Caml. http://www.lri.fr/~filliatr/ocamlweb/. [ bib  http ] 
[1] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
http://why3.lri.fr/.
[ bib ]
Keywords: Why3 
Back
This page was generated by bibtex2html.