[1] | Albin Coquereau, Sylvain Conchon, Mohamed Iguernlala, Alain Mebsout. Alt-Ergo 2.2. In International Workshop on Satisfiability Modulo Theories (SMT 2018), to appear, Oxford, UK, July 2018. [ bib | .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 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 ] |
[11] | 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 ] |
[12] | 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 ] |
[13] | 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 ] |
[14] | Mário Pereira. Défonctionnaliser pour prouver. In Boldo and Signoles [15]. [ bib | full text on HAL ] |
[15] | Sylvie Boldo and Julien Signoles, editors. Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
[16] |
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 |
[17] | Arthur Charguéraud and Mike Rainey. Efficient representations for large dynamic sequences in ml. In ML Family Workshop, 2017. [ bib | full text on HAL ] |
[18] | 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 ] |
[19] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. 60(3):365--383, 2018. [ bib | DOI | full text on HAL ] |
[20] | 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 [21]. [ bib | full text on HAL | .pdf ] |
[21] | 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 ] |
[22] | 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 ] |
[23] | 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 [24]. [ bib | full text on HAL ] |
[24] | Annabelle McIver and Maurice ter Beek, editors. FM 2019 23rd International Symposium on Formal Methods, October 2019. [ bib ] |
[25] | The VOCaL project. The VOCaL library. Open Source Software, with MIT license, 2018. https://github.com/vocal-project/vocal. [ bib ] |
[26] | TrustInSoft. Report on the deployment of the VOCaL library in TrustInSoft kernel, May 2019. [ bib ] |
This file was generated by bibtex2html 1.99.