Publications : Jean-Christophe Filliâtre
Back[128] | Jean-Christophe Filliâtre. Simpler proofs with decentralized invariants. Journal of Logical and Algebraic Methods in Programming, January 2021. See http://why3.lri.fr/spdi/. [ bib | DOI | full text on HAL ] |
[127] | Jean-Christophe 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 122--142, Rhodes, Greece, October 2020. Springer. http://why3.lri.fr/isola-2020/. [ bib | full text on HAL ] |
[126] | Jean-Christophe 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 ] |
[125] | 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 ] |
[124] | Jean-Christophe Filliâtre. Mesurer la hauteur d'un arbre. In Zaynah Dargaye and Yann Régis-Gianas, editors, Trente-et-unièmes Journées Francophones des Langages Applicatifs, Gruissan, France, January 2020. https://www.lri.fr/~filliatr/hauteur/. [ bib | full text on HAL | Slides ] |
[123] | 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 ] |
[122] | Jean-Christophe 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, Jean-Christophe Filliâtre, Cláudio 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, Jean-Christophe Filliâtre, and Kim Nguyen. Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Ellipses, August 2019. [ bib | http ] |
[119] | Jean-Christophe Filliâtre. The Why3 tool for deductive verification and verified OCaml libraries. In Frama-C & SPARK Day 2019, Paris, France, June 2019. Invited talk. [ bib ] |
[118] | Jean-Christophe 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] | Jean-Christophe Filliâtre. Parcours d'un informaticien. Séminaire Info Pour Tous, September 2018. Séminaire invité. [ bib | http ] |
[116] | Jean-Christophe Filliâtre. Auto-active verification using Why3's IDE. In 4th Workshop on Formal Integrated Development Environment, Oxford, UK, July 2018. Invited talk. [ bib ] |
[115] | Jean-Christophe Filliâtre. An introduction to deductive program verification. Mathematical Summer in Paris (summer school), July 2018. Cours invité. [ bib ] |
[114] | Jean-Christophe 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 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science. Springer, 2018. Invited talk. [ bib ] |
[113] | Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, and Simão Melo de Sousa. A toolchain to Produce Correct-by-Construction OCaml Programs. Technical report, 2018. artifact: https://www.lri.fr/~mpereira/correct_ocaml.ova. [ bib | full text on HAL | .pdf ] |
[112] | Jean-Christophe 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, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ] |
[111] | Jean-Christophe Filliâtre. Why3 --- where programs meet provers. In KeY Symposium 2017, Rastatt, Germany, October 2017. Invited talk. [ bib ] |
[110] | Arthur Charguéraud, Jean-Christophe 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] | Jean-Christophe 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] | Jean-Christophe Filliâtre. Why3 tutorial. In VerifyThis 2017, Uppsala, Sweden, April 2017. Invited tutorial. [ bib ] |
[107] | Jean-Christophe 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] |
Jean-Christophe 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 non-deterministic 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 higher-order 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] |
Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
A pragmatic type system for deductive verification.
Research report, Université Paris Sud, 2016.
https://hal.archives-ouvertes.fr/hal-01256434v3.
[ 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. |
[104] | Jean-Christophe Filliâtre and Mário Pereira. Itérer avec confiance. In Vingt-septièmes Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016. [ bib | full text on HAL ] |
[103] |
Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
The spirit of ghost code.
Formal Methods in System Design, 48(3):152--174, 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 state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. Keywords: Why3 |
[102] |
Martin Clochard, Jean-Christophe 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 94--109, San
Francisco, California, USA, July 2015. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
[101] | 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.lri.fr/download/manual-0.86.1.pdf. [ bib | .pdf ] |
[100] | Jean-Christophe Filliâtre. Vérification déductive de programmes. Mathematic Park, Institut Henri Poincaré, March 2015. Séminaire invité. [ bib | http ] |
[99] | 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.lri.fr/gallery/fm2012comp.en.html. [ bib | DOI | full text on HAL ] |
[98] | Sylvain Conchon and Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, September 2014. [ bib | full text on HAL | http ] |
[97] |
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 |
[96] |
Jean-Christophe 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 1--16, 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 state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. Keywords: Why3 |
[95] | Jean-Christophe 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 ] |
[94] | Jean-Christophe Filliâtre. Démonstration. l'ordinateur à la rescousse. Tangente (hors-série numéro 52), (52):34--36, February 2014. [ bib ] |
[93] | Jean-Christophe Filliâtre. Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml. In Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. https://www.lri.fr/~filliatr/publis/bouturage.pdf. [ bib ] |
[92] | Sylvie Boldo, François Clément, Jean-Christophe 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):325--352, 2014. [ bib | DOI | full text on HAL | http ] |
[91] | 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.lri.fr/download/manual-0.82.pdf. [ bib | .pdf ] |
[90] | Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco, Gilles Dowek, Jean-Christophe 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] |
Jean-Christophe Filliâtre.
One logic to use them all.
In 24th International Conference on Automated Deduction
(CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence,
pages 1--20, Lake Placid, USA, June 2013. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
[88] | Jean-Christophe Filliâtre. Deductive program verification with Why3. In MSR-Inria Joint Centre “Spring Day”, Lyon, France, May 2013. Invited talk. [ bib ] |
[87] |
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 |
[86] | Sylvie Boldo, François Clément, Jean-Christophe 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):423--456, April 2013. [ bib | DOI | full text on HAL ] |
[85] |
Jean-Christophe 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 125--128. Springer, March 2013.
[ bib |
full text on HAL ]
Keywords: Why3 |
[84] | Jean-Christophe Filliâtre and Andrei Paskevich. Why3 --- where programs meet provers. In ESOP [85], pages 125--128. [ bib ] |
[83] |
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.lri.fr/download/manual-0.81.pdf.
[ bib |
full text on HAL |
.pdf ]
Keywords: Why3 |
[82] | Jean-Christophe Filliâtre and Rémy El Sibaïe. Combine : une bibliothèque OCaml pour la combinatoire. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://www.lri.fr/~filliatr/combine/. [ bib | full text on HAL | .pdf ] |
[81] |
Jean-Christophe 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 |
[80] | Jean-Christophe 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 ] |
[79] |
François Bobot and Jean-Christophe Filliâtre.
Separation predicates: a taste of separation logic in first-order
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 first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3. |
[78] | José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Science of Computer Programming, October 2012. Accepted for publication. [ bib | DOI ] |
[77] |
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 |
[76] |
Mário Pereira, Jean-Christophe 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 (low-level) 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] | Jean-Christophe 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 ] |
[73] |
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 |
[72] |
Jean-Christophe Filliâtre.
Course notes EJCP 2012, chapter Vérification déductive de
programmes avec Why3.
June 2012.
[ bib |
http ]
Keywords: Why3 |
[71] |
Jean-Christophe 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 8--10, 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] |
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. |
[69] |
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 |
[68] | Jean-Christophe 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] | 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 ] |
[66] |
Jean-Christophe 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 83--97, Philadelphia, USA, January 2012. Springer.
[ bib |
.pdf ]
This article details the formal verification of a 2-line C program that computes the number of solutions to the n-queens 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 (Alt-Ergo, 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 |
[65] |
Sylvie Boldo, François Clément, Jean-Christophe 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 one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off 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 machine-checked. 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 |
[64] | Jean-Christophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université Paris-Sud, December 2011. [ bib | .pdf ] |
[63] | Jean-Christophe 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, 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 |
[61] |
Jean-Christophe Filliâtre.
Deductive software verification.
International Journal on Software Tools for Technology Transfer
(STTT), 13(5):397--403, 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. |
[60] |
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 |
[59] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie [60], pages 53--64. https://hal.inria.fr/hal-00790310. [ bib ] |
[58] |
Claire Dross, Jean-Christophe 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 102--118,
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 ad-hoc data structures based on pointers. As standards like DO-178C 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 user-provided 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] |
Jean-Christophe 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 65--81, 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, multi-core or network, and (3) a reliable fault-tolerance 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, 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.lri.fr/.
[ bib ]
Keywords: Why3 |
[55] | Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ] |
[54] | Manuel Barbosa, Jean-Christophe 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] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the First Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147--162, Edinburgh, Scotland, July 2010. Springer. [ bib | DOI | full text on HAL ] |
[52] | Jean-Christophe Filliâtre and Claude Marché. Bibtex2html. APP Deposit, 2010. [ bib ] |
[51] | Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation temps-réel de programmes Caml. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ] |
[50] |
Johannes Kanig and Jean-Christophe Filliâtre.
Who: A Verifier for Effectful Higher-order 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 higher-order functions. It features Effect polymorphism, higher-order 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 ML-like programming languages. |
[49] | Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 59--74, Grand Bend, Canada, July 2009. Springer. [ bib | DOI ] |
[48] |
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane
Lescuyer.
Faire bonne figure avec Mlpost.
In Vingtièmes Journées Francophones des Langages
Applicatifs, Saint-Quentin 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. |
[47] | 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 ] |
[46] | Jean-Christophe 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 ] |
[45] |
Jean-Christophe Filliâtre.
A Functional Implementation of the Garsia--Wachs 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 Garsia--Wachs 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, pattern-matching, polymorphism) and nicely compares to the purely imperative implementation from The Art of Computer Programming. |
[44] | 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 ] |
[43] | Jean-Christophe 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 ] |
[42] |
Jean-Christophe Filliâtre.
Gagner en passant à la corde.
In Dix-neuviè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 au-delà 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] | Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | PDF | .pdf ] |
[40] | Sylvain Conchon, Jean-Christophe 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 ] |
[39] |
Jean-Christophe 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. |
[38] |
Sylvain Conchon and Jean-Christophe Filliâtre.
A Persistent Union-Find Data Structure.
In ACM SIGPLAN Workshop on ML, pages 37--45, Freiburg, Germany,
October 2007. ACM Press.
[ bib |
PDF |
.pdf ]
The problem of disjoint sets, also known as union-find, 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 union-find 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. |
[37] | 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 ] |
[36] |
Sylvie Boldo and Jean-Christophe Filliâtre.
Formal Verification of Floating-Point Programs.
In 18th IEEE International Symposium on Computer Arithmetic,
pages 187--194, Montpellier, France, June 2007.
[ bib |
PDF |
.pdf ]
This paper introduces a methodology to perform formal verification of floating-point C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floating-point arithmetic. The Caduceus first-order 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 floating-point arithmetic. This methodology is already implemented and has been successfully applied to several short floating-point programs, which are presented in this paper. |
[35] | Sylvain Conchon, Jean-Christophe 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] |
Sylvain Conchon, Jean-Christophe 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 TR-SHU-CS-2007-04-1,
pages XII/1--13, 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 structures---directed 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 so-called functors. |
[33] | Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification, 2007. http://why.lri.fr/queens/. [ bib | PDF | http ] |
[32] |
Sylvain Conchon and Jean-Christophe Filliâtre.
Union-Find Persistant.
In Dix-huitièmes Journées Francophones des Langages
Applicatifs, pages 135--149. INRIA, January 2007.
[ bib |
PDF |
.pdf ]
Le problème des classes disjointes, connu sous le nom de union-find, 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. |
[31] | Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ] |
[30] | Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ] |
[29] |
Nicolas Ayache and Jean-Christophe Filliâtre.
Combining the Coq proof assistant with first-order decision
procedures.
http://www.lri.fr/~filliatr/publis/coq-dp.ps.gz, March 2006.
[ bib |
.ps.gz ]
We present an integration of first-order automatic theorem provers into the Coq proof assistant. This integration is based on a translation from the higher-order logic of Coq, the Calculus of Inductive Constructions, to a polymorphic first-order logic. This translation is defined and proved sound in this paper. It includes not only the translation of terms and predicates belonging to the first-order fragment, but also several techniques to go well beyond: abstractions of higher-order sub-terms, case-analysis, 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] | Jean-Christophe Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332--240, 2006. [ bib | DOI | PDF | .pdf ] |
[27] | Jean-Christophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib | .ps.gz ] |
[26] | Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs. INRIA, January 2006. [ bib | .ps.gz ] |
[25] | Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 79--94. INRIA, March 2005. [ bib | .ps.gz ] |
[24] | Jean-Christophe 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 370--384, Barcelona, Spain, April 2004. [ bib | PDF | .pdf ] |
[23] | 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 ] |
[22] | 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 ] |
[21] | Jean-Christophe Filliâtre and F. Pottier. Producing All Ideals of a Forest, Functionally. Journal of Functional Programming, 13(5):945--956, September 2003. [ bib | PDF ] |
[20] | Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, July 2003. [ bib | .ps.gz ] |
[19] | Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, July 2003. [ bib | PDF | .pdf ] |
[18] | Jean-Christophe Filliâtre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz. [ bib | .ps.gz ] |
[17] | Jean-Christophe Filliâtre, Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2003. http://krakatoa.lri.fr/. [ bib ] |
[16] | Jean-Christophe Filliâtre. La supériorité de l'ordre supérieur. In Journées Francophones des Langages Applicatifs, pages 15--26, Anglet, France, January 2002. [ bib | PDF | .pdf ] |
[15] | Jean-Christophe Filliâtre. The Why verification tool, 2002. http://why.lri.fr/. [ bib | http ] |
[14] | Jean-Christophe 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 246--249. Springer, 2001. [ bib ] |
[13] | Jean-Christophe 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] | Jean-Christophe Filliâtre. Hash consing in an ML framework. Research Report 1368, LRI, Université Paris Sud, September 2000. [ bib | .ps.gz ] |
[11] | Jean-Christophe Filliâtre. A theory of monads parameterized by effects. Research Report 1367, LRI, Université Paris Sud, November 1999. [ bib | .ps.gz ] |
[10] | Jean-Christophe Filliâtre. Preuve de programmes impératifs en théorie des types. PhD thesis, Université Paris-Sud, July 1999. [ bib | .ps.gz ] |
[9] | 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 ] |
[8] | Jean-Christophe 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. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.2. INRIA-Rocquencourt-CNRS-Université Paris Sud- ENS Lyon, May 1998. [ bib | ftp ] |
[6] | Jean-Christophe 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] | Jean-Christophe 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] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
http://why3.lri.fr/.
[ bib ]
Keywords: Why3 |
[3] | Jean-Christophe Filliâtre and Claude Marché. Ocamlweb, a literate programming tool for Objective Caml. http://www.lri.fr/~filliatr/ocamlweb/. [ bib | http ] |
[2] | Sylvain Conchon and Jean-Christophe Filliâtre. Semi-persistent data structures. Technical report. [ bib ] |
[1] | Jean-Christophe Filliâtre, Thierry Hubert, and Claude Marché. The Caduceus tool for the verification of C programs. http://caduceus.lri.fr/. [ bib ] |
Back
This page was generated by bibtex2html.