[1] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In SMT Workshop: International Workshop on Satisfiability Modulo Theories, Oxford, United Kingdom, July 2018. [ bib | http | .pdf ]
[2] Jean-Christophe Filliâtre and Mário Pereira. Itérer avec confiance. In Vingt-septièmes Journées Francophones des Langages Applicatifs [6]. [ bib | full text on HAL ]
[3] Jean-Christophe Filliâtre and Mário Pereira. A modular way to reason about iteration. In 8th NASA Formal Methods Symposium [8]. [ 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.
[4] Jean-Christophe Filliâtre and Mário Pereira. Producing all ideals of a forest, formally (verification pearl). In Blazy and Chechik [7]. [ bib | full text on HAL ]
[5] Martin Clochard, Léon Gondelman, and Mário Pereira. The matrix reproved. In Blazy and Chechik [7]. [ bib | full text on HAL ]
[6] Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016. [ bib ]
[7] Sandrine Blazy and Marsha Chechik, editors. VSTTE 2016, Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib ]
[8] volume 9690 of Lecture Notes in Computer Science, Minneapolis, MN, USA, June 2016. Springer. [ bib ]
[9] Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In Proceedings of the 6th Conference on Interactive Theorem Proving (ITP 2015), volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, August 2015. [ bib | .pdf ]
[10] Arthur Charguéraud. Higher-order representation predicates in separation logic. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, page 3–14, New York, NY, USA, 2016. Association for Computing Machinery. [ bib | DOI | http ]
Keywords: Representation Predicates, Separation Logic
[11] Arthur Charguéraud and François Pottier. Temporary read-only permissions for separation logic. In Hongseok Yang, editor, Proceedings of the European Symposium on Programming (ESOP 2017), Lecture Notes in Computer Science. Springer, April 2017. [ bib | .pdf ]
[12] François Pottier. Verifying a hash table and its iterators in higher-order separation logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pages 3--16, January 2017. [ bib | .pdf ]
[13] Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, September 2017. [ bib | full text on HAL | .pdf ]
[14] 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 ]
[15] Mário Pereira. Défonctionnaliser pour prouver. In Boldo and Signoles [16]. [ bib | full text on HAL ]
[16] Sylvie Boldo and Julien Signoles, editors. Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[17] Sylvain Boulmé and Alexandre Maréchal. Toward Certification for Free! working paper or preprint, July 2017. [ bib | http | .pdf ]
Keywords: Linear Programming ; Coq ; Type theory ; Abstract Domain of Polyhedra ; Polymorphism ; Program verification ; Parametricity ; CCS Concepts: Software and its engineering -> Polymorphism ; Theory of computation -> Program veriication ; Invariants ; Mathematics of computing -> Solvers ; Additional Key Words and Phrases: Abstract Domain of Polyhedra ; CCC
[18] Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, and Hang Yu. The Verified Polyhedron Library: an overview. In Erika Ábrahám, Viorel Negru, Dana Petcu, Daniela Zaharie, Tetsuo Ida, Tudor Jebelean, and Stephen Watt, editors, 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 9--17, Timișoara, Romania, September 2018. Universitatea de Vest din Timișoara, IEEE Computer Society. [ bib | http ]
[19] Sylvain Boulmé and Alexandre Maréchal. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Journal of Automated Reasoning, November 2018. [ bib | DOI | http ]
Keywords: Continuation-Passing Style ; Linear arithmetic ; Refinement calculus ; Abstract Interpretation ; The Coq proof assistant ; Monad ; Weakest precondition ; Certified Software ; Proof Assistants ; Result Certification
[20] Cyril Six, Sylvain Boulmé, and David Monniaux. Certified and efficient instruction scheduling. Application to interlocked VLIW processors. Proceedings of the ACM on Programming Languages, page 129, November 2020. [ bib | DOI | http ]
[21] Arthur Charguéraud and Mike Rainey. Efficient representations for large dynamic sequences in ML. In ML Family Workshop, 2017. [ bib | full text on HAL ]
[22] Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In Amal Ahmed, editor, Proceedings of the European Symposium on Programming (ESOP 2018), volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, April 2018. [ bib | .pdf ]
[23] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. 60(3):365--383, 2018. [ bib | DOI | full text on HAL ]
[24] Jean-Christophe Filliâtre, Mário Pereira, and Simão Melo de Sousa. Vérification de programmes fortement impératifs avec Why3. In Boldo and Magaud [25]. [ bib | full text on HAL | .pdf ]
[25] 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 ]
[26] 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. https://hal.inria.fr/hal-01783851. [ bib | full text on HAL | .pdf ]
[27] Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. Mosel: A general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2(ICFP), July 2018. [ bib | DOI | http ]
Keywords: modal logic, Coq proof assistant, logic of bunched implications, Separation logic, interactive theorem proving
[28] Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, and Mário Pereira. GOSPEL --- providing OCaml with a formal specification language. In McIver and ter Beek [29]. [ bib | full text on HAL ]
[29] Annabelle McIver and Maurice ter Beek, editors. FM 2019 23rd International Symposium on Formal Methods, October 2019. [ bib ]
[30] The VOCaL project. The VOCaL library. Open Source Software, with MIT license, 2018. https://github.com/vocal-project/vocal. [ bib ]
[31] TrustInSoft. Report on the deployment of the VOCaL library in TrustInSoft kernel, May 2019. [ bib ]
[32] Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1--27. Springer, April 2019. [ bib | .pdf ]
[33] Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan. Spy game: Verifying a local generic solver in Iris. Proceedings of the ACM on Programming Languages, 4(POPL), January 2020. [ bib | .pdf ]
We verify the partial correctness of a “local generic solver”, that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for “spying”, a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley's modulus function, an archetypical example of spying.
[34] Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1--18:20, Dagstuhl, Germany, 2019. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | http ]
[35] Dominique Larchey-Wendling and Jean-François Monin. Simulating induction-recursion for partial algorithms. In Josè Espìrito Santo and Luìs Pinto, editors, TYPES 2018 Abstracts, Braga, June 2018. [ bib | .pdf ]
We describe a generic method to implement and extract partial recursive algorithms in Coq in a purely constructive way, using L. Paulson's if-then-else normalization as a running example.
[36] Yuxin Deng and Jean-François Monin. Formalisation of probabilistic testing semantics in coq. In Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, and Frank Valencia, editors, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, volume 11760 of Lecture Notes in Computer Science, pages 276--292. Springer, 2019. [ bib | .pdf ]
Van Breugel et al. [F. van Breugel et al, Theor. Comput. Sci. 333(1-2):171-197, 2005] have given an elegant testing framework that can characterise probabilistic bisimulation, but its completeness proof is highly involved. Deng and Feng [Y. Deng and Y. Feng, Inf. Comput. 257:58-64, 2017] have simplified that result for finite-state processes. The crucial part in the latter work is an algorithm that can construct enhanced tests. We formalise the algorithm and prove its correctness by maintaining a number of subtle invariants in Coq. To support the formalisation, we develop a reusable library for manipulating finite sets. This sets an early example of formalising probabilistic concurrency theory or quantitative aspects of concurrency theory at large, which is a rich field to be pursued
[37] 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 ]
[38] 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 ]
[39] Glen Mével, Jacques-Henri Jourdan, and François Pottier. Cosmo: A concurrent separation logic for Multicore OCaml. Proceedings of the ACM on Programming Languages, 4(ICFP), June 2020. [ bib | .pdf ]
[40] Arthur Charguéraud. Separation logic for sequential programs (functional pearl). Proc. ACM Program. Lang., 4(ICFP), August 2020. [ bib | DOI | http ]
Keywords: Separation Logic, Coq, Program verification
[41] Paulo Emílio de Vilhena and François Pottier. A separation logic for effect handlers. Proceedings of the ACM on Programming Languages, 5(POPL), January 2021. [ bib | .pdf ]
[42] François Pottier. Strong automated testing of OCaml libraries. In Journées Francophones des Langages Applicatifs (JFLA), February 2021. [ bib | .pdf ]
[43] Dominique Larchey-Wendling and Jean-François Monin. The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq, chapter 8, pages 305--386. In Mainzer et al. [44], September 2021. [ bib ]
[44] Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors. Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification. World Scientific, September 2021. [ bib ]
[45] Jean-Christophe Filliâtre and Clément Pascutto. Ortac: Runtime assertion checking for OCaml. Technical report, Université Paris-Saclay, 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.
[46] 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 ]
[47] 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 ]

This file was generated by bibtex2html 1.99.