Publications since 2004
BackBooks / Journals / Conferences / PhD theses / Misc. / Reports
Books and book chapters
[25] | Allan Blanchard, Claude Marché, and Virgile Prevosto. Guide to Software Verification with Frama-C --- Core Components, Usages, and Applications, chapter Formally Expressing what a Program Should Do: the ACSL Language, pages 3--80. Springer-Verlag, 2024. [ bib | DOI | full text on HAL ] |
[24] | Thibaut Balabonski, Sylvain Conchon, Jean-Christophe 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 ] |
[23] | Thibaut Balabonski, Sylvain Conchon, Jean-Christophe 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 ] |
[22] | Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, and Kim Nguyen. Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Première. Ellipses, 2019. [ bib | full text on HAL ] |
[21] |
Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre
Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie
Revol, and Serge Torres.
Handbook of Floating-point Arithmetic (2nd edition).
Birkhäuser Basel, July 2018.
[ bib |
DOI |
full text on HAL ]
Keywords: arithmetic operators ; arithmetic algorithms ; numerical computing ; floating-point arithmetic ; computer arithmetic |
[20] | Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, December 2017. [ bib | full text on HAL ] |
[19] |
Christine Paulin-Mohring.
Introduction to the Calculus of Inductive Constructions.
In Bruno Woltzenlogel Paleo and David Delahaye, editors, All
about Proofs, Proofs for All, volume 55 of Studies in Logic
(Mathematical logic and foundations). College Publications, January 2015.
[ bib |
http |
.pdf ]
Keywords: Coq proof assistant ; Calculus of Inductive Constructions |
[18] | Sylvie Boldo. Même les ordinateurs font des erreurs ! In Martin Andler, Liliane Bel, Sylvie Benzoni-Gavage, Thierry Goudon, Cyril Imbert, and Antoine Rousseau, editors, Brèves de maths, pages 136--137. Nouveau Monde Editions, October 2014. [ bib | full text on HAL | http ] |
[17] | 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 ] |
[16] | 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 ] |
[15] | Sylvie Boldo and Guillaume Melquiond. Informatique Mathématique, une photographie en 2013, chapter Arithmétique des ordinateurs et preuves formelles, pages 189--220. Presses Universitaires de Perpignan, Perpignan, France, 2013. [ bib | full text on HAL ] |
[14] |
Jean-Christophe Filliâtre.
Course notes EJCP 2012, chapter Vérification déductive de
programmes avec Why3.
June 2012.
[ bib |
http ]
Keywords: Why3 |
[13] | Sylvie Boldo and Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. In Valérie Berthé, Christiane Frougny, Natacha Portier, Marie-Françoise Roy, and Anne Siegel, editors, École des Jeunes Chercheurs en Informatique Mathématique, pages 1--30. Rennes, France, March 2012. [ bib | full text on HAL ] |
[12] | Christine Paulin-Mohring. Tools for practical software verification (international summer school, LASER 2011, revised tutorial lectures). volume 7682 of Lecture Notes in Computer Science, chapter Introduction to the Coq proof-assistant for practical software verification. Springer, 2012. [ bib | .pdf ] |
[11] | Sylvie Boldo and Thierry Viéville. Représentation numérique de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 23--72. CRDP Académie de Paris, July 2011. [ bib | http ] |
[10] | Sylvie Boldo and Thierry Viéville. Structuration et contrôle de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 281--308. CRDP Académie de Paris, July 2011. [ bib | http ] |
[9] | Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. [ bib ] |
[8] | V. Benzaken, G. Castagna, H. Hosoya, B.C. Pierce, and S. Vansummeren. The Encyclopedia of Database Systems, chapter “XML Typechecking”. Springer, 2009. Invited Article. [ bib ] |
[7] | Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. In Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors, From Semantics to Computer Science: Essays in Honor of Gilles Kahn. Cambridge University Press, 2009. [ bib | full text on HAL | PDF ] |
[6] | Sylvie Boldo. Demandez le programme! In DocSciences, volume 5, pages 26--33. C.R.D.P. de l'académie de Versailles, November 2008. http://www.docsciences.fr/-DocSciences-no5-. [ bib | http ] |
[5] | 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 8th International Symposium on Trends in Functional Programming (TFP'07), New York, USA, volume 8. Intellect, 2008. [ bib ] |
[4] | Paul Caspi, Grégoire Hamon, and Marc Pouzet. Real-Time Systems: Models and verification --- Theory and tools, chapter Synchronous Functional Programming with Lucid Synchrone. ISTE, 2007. [ bib ] |
[3] | Évelyne Contejean. Modelling permutations in Coq for Coccinelle. In Hubert Comon-Lundth, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 259--269. Springer, 2007. Jouannaud Festschrift. [ bib | DOI | Abstract ] |
[2] | Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235--258. Springer, 2007. [ bib ] |
[1] | Paul Caspi, Grégoire Hamon, and Marc Pouzet. Systèmes Temps-réel : Techniques de Description et de Vérification -- Théorie et Outils, volume 1, chapter Lucid Synchrone, un langage de programmation des systèmes réactifs, pages 217--260. Hermes, 2006. [ bib ] |
Journals
[76] | Léo Andrès, Filipe Marques, Arthur Carcano, Pierre Chambart, José Fragoso Femenin dos Santos, and Jean-Christophe Filliâtre. Owi: Performant parallel symbolic execution made easy, an application to WebAssembly. The Art, Science, and Engineering of Programming, 9(2), 2024. [ bib | full text on HAL ] |
[75] | Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. Journal of Symbolic Computation, 115:74--95, 2023. [ bib | DOI | full text on HAL ] |
[74] | Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. Cerise: Program verification on a capability machine in the presence of untrusted code. Journal of the ACM, 2023. [ bib | DOI | full text on HAL ] |
[73] | Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, and Jean-Michel Muller. Floating-point arithmetic. Acta Numerica, 32:203--290, 2023. [ bib | DOI | full text on HAL ] |
[72] | Érik Martin-Dorel, Guillaume Melquiond, and Pierre Roux. Enabling floating-point arithmetic in the Coq proof assistant. Journal of Automated Reasoning, 67(33), 2023. [ bib | DOI | full text on HAL ] |
[71] | Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. Logical Methods in Computer Science, 19(1), 2023. [ bib | DOI | full text on HAL ] |
[70] | Sylvie Boldo, Nicolas Brisebarre, and Jean-Michel Muller. Le dilemme du fabricant de tables. La Recherche, 572, 2023. [ bib | full text on HAL ] |
[69] |
Louise Ben Salem-Knapp, Sylvie Boldo, and William Weens.
Bounding the round-off error of the upwind scheme for advection.
IEEE Transactions on Emerging Topics in Computing, 10(3), 2022.
[ bib |
DOI |
full text on HAL ]
Keywords: Round-off error ; Floating-Point ; Numerical Scheme ; Advection ; Hydrodynamics |
[68] |
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude
Marché, David Mentré, and Hiroaki Inoue.
Automated formal analysis of temporal properties of Ladder
programs.
International Journal on Software Tools for Technology
Transfer, 24(6):977--997, 2022.
[ bib |
DOI |
full text on HAL ]
Keywords: Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment |
[67] | Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. The CoLiS platform for the analysis of maintainer scripts in Debian software packages. International Journal on Software Tools for Technology Transfer, 2022. [ bib | full text on HAL ] |
[66] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. Journal of Automated Reasoning, 66:175--213, 2022. [ bib | DOI | full text on HAL ] |
[65] | Jean-Christophe Filliâtre. Simpler proofs with decentralized invariants. Journal of Logical and Algebraic Methods in Programming, 121, January 2021. See https://usr.lmf.cnrs.fr/~jcf/spdi/. [ bib | DOI | full text on HAL ] |
[64] | Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller. Emulating round-to-nearest ties-to-zero ”augmented” floating-point operations using round-to-nearest ties-to-even arithmetic. IEEE Transactions on Computers, 70(7):1046--1058, 2021. [ bib | DOI | full text on HAL ] |
[63] | Florian Steinberg, Laurent Théry, and Holger Thies. Computable analysis and notions of continuity in Coq. Logical Methods in Computer Science, 2021. [ bib | DOI | full text on HAL ] |
[62] | Sylvain Conchon, Giorgio Delzanno, and Angelo Ferrando. Declarative parameterized verification of distributed protocols via the cubicle model checker. Fundam. Informaticae, 178(4):347--378, 2021. [ bib | DOI ] |
[61] | Sylvain Conchon, David Declerck, and Fatiha Zaïdi. Parameterized model checking on the TSO weak memory model. Journal of Automated Reasoning, 64(7):1307--1330, 2020. [ bib | full text on HAL ] |
[60] | Diane Gallois-Wong, Sylvie Boldo, and Pascal Cuoq. Optimal inverse projection of floating-point addition. Numerical Algorithms, 83(3):957--986, 2020. [ bib | DOI | full text on HAL ] |
[59] |
Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller.
Emulating round-to-nearest ties-to-zero ”augmented” floating-point
operations using round-to-nearest ties-to-even arithmetic.
Transactions on Computers, 2020.
[ bib |
DOI |
full text on HAL ]
Keywords: Numerical reproducibility ; Floating-point arithmetic ; Numerical repro- ducibility ; Formal proof ; Rounding mode ; Error-free transforms ; Rounding error analysis |
[58] | Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. Journal of Automated Reasoning, 62(2):281--300, February 2019. [ bib | DOI | full text on HAL ] |
[57] | Diane Gallois-Wong, Sylvie Boldo, and Pascal Cuoq. Optimal inverse projection of floating-point addition. Numerical Algorithms, 2019. [ bib | DOI | full text on HAL | .pdf ] |
[56] | Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, 2019. [ bib | DOI | full text on HAL | .pdf ] |
[55] | Eike Neumann and Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. Theoretical Computer Science, 2019. [ bib | DOI | full text on HAL ] |
[54] | Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, 2019. [ bib | DOI | full text on HAL ] |
[53] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. Journal of Automated Reasoning, 60(3):365--383, 2018. [ bib | DOI | full text on HAL ] |
[52] |
Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy.
Instrumenting a weakest precondition calculus for counterexample
generation.
Journal of Logical and Algebraic Methods in Programming,
99:97--113, 2018.
[ bib |
DOI |
full text on HAL ]
Keywords: Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples |
[51] |
Anastasia Volkova, Matei Istoan, Florent de Dinechin, and Thibault Hilaire.
Towards hardware IIR filters computing just right: Direct form I
case study.
IEEE Transactions on Computers, 2018.
[ bib |
full text on HAL ]
Keywords: computer arithmetic ; fixed-point ; FPGA ; error analysis ; digital filters ; constant multiplication |
[50] | Sylvie Boldo, Stef Graillat, and Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, 44(1), July 2017. [ bib | full text on HAL | .pdf ] |
[49] | Ran Chen, Martin Clochard, and Claude Marché. A formally proved, complete algorithm for path resolution with symbolic links. Journal of Formalized Reasoning, 10(1):51--66, 2017. [ bib | DOI | full text on HAL | http ] |
[48] | Umut A Acar, Arthur Charguéraud, and Mike Rainey. Oracle-guided scheduling for controlling granularity in implicitly parallel languages. Journal of Functional Programming, 26, November 2016. [ bib | DOI | full text on HAL ] |
[47] | Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 2016. [ bib | full text on HAL ] |
[46] |
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Journal of Automated Reasoning, 56(4):387--457, 2016.
[ bib |
full text on HAL ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists.
|
[45] |
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 |
[44] |
Érik Martin-Dorel and Guillaume Melquiond.
Proving tight bounds on univariate expressions with elementary
functions in Coq.
Journal of Automated Reasoning, 2016.
[ bib |
DOI |
full text on HAL ]
Keywords: Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic |
[43] | Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41--62, June 2015. [ bib | DOI | full text on HAL ] |
[42] | Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135--163, February 2015. [ bib | full text on HAL ] |
[41] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709--727, 2015. See also http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html. [ bib | DOI | full text on HAL ] |
[40] | Claude Marché and Johannes Kanig. Bridging the gap between testing and formal verification in Ada development. ERCIM News, 100:38--39, January 2015. [ bib | full text on HAL ] |
[39] |
Pierre Roux.
Formal proofs of rounding error bounds.
Journal of Automated Reasoning, 2015.
[ bib |
DOI |
full text on HAL ]
Keywords: floating-point arithmetic ; rounding error ; numerical analysis ; proof assistant ; Coq ; matrices ; Cholesky decomposition |
[38] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, 54(1):1--29, 2015.
[ bib |
DOI |
full text on HAL ]
Keywords: formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic |
[37] | Sylvie Boldo and Jean-Michel Muller. Des ordinateurs capables de calculer plus juste. La Recherche, 492:46--52, October 2014. [ bib | full text on HAL ] |
[36] |
Claude Marché.
Verification of the functional behavior of a floating-point program:
an industrial case study.
Science of Computer Programming, 96(3):279--296, March 2014.
[ bib |
DOI |
full text on HAL |
.pdf ]
We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving
|
[35] | Jean-Christophe Filliâtre. Démonstration. l'ordinateur à la rescousse. Tangente (hors-série numéro 52), (52):34--36, February 2014. [ bib ] |
[34] | 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 ] |
[33] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, pages 1--29, 2014.
[ bib |
DOI |
full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic |
[32] | 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 ] |
[31] | Véronique Benzaken, Giuseppe Castagna, Dario Colazzo, and Kim Nguyen. Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems (TODS), 2013. [ bib | full text on HAL ] |
[30] | Guillaume Melquiond, Werner Georg Nowak, and Paul Zimmermann. Numerical approximation of the Masser-Gramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 82:1235--1246, 2013. [ bib | DOI | full text on HAL ] |
[29] |
Diego Arroyuelo, Francisco Claude, Sebastian Maneth, Veli Mäkinen, Gonzalo
Navarro, Kim Nguyen, Jouni Sirén, and Niko Välimäki.
Fast in-memory XPath search using compressed indexes.
Software: Practice and Experience, pages n/a--n/a, 2013.
[ bib |
DOI ]
Keywords: XML, succinct data structures, XPath, tree automata |
[28] | Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, 53(4):897--924, 2013. [ bib | DOI | full text on HAL ] |
[27] | 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 ] |
[26] | Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation. Logical Methods in Computer Science, 8(3):1--29, September 2012. Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany, 2011. [ bib | DOI | full text on HAL | http ] |
[25] | Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14--23, 2012. [ bib | DOI | full text on HAL ] |
[24] |
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.
|
[23] |
Sylvie Boldo and Jean-Michel Muller.
Exact and Approximated error of the FMA.
IEEE Transactions on Computers, 60(2):157--164, February 2011.
[ bib |
full text on HAL ]
The fused multiply accumulate-add (FMA) instruction, specified by the IEEE 754-2008 Standard for Floating-Point Arithmetic, eases some calculations, and is already available on some current processors such as the Power PC or the Itanium. We first extend an earlier work on the computation of the exact error of an FMA (by giving more general conditions and providing a formal proof). Then, we present a new algorithm that computes an approximation to the error of an FMA, and provide error bounds and a formal proof for that algorithm.
|
[22] | Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242--253, 2011. [ bib | DOI | full text on HAL ] |
[21] | Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151--160, 2011. [ bib | full text on HAL ] |
[20] | Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377--393, 2011. [ bib | DOI | full text on HAL ] |
[19] | Marc Pouzet and Pascal Raymond. Modular Static Scheduling of Synchronous Data-flow Networks: An efficient symbolic representation. Journal of Design Automation for Embedded Systems, 2010. Special issue of selected papers from http://esweek09.inrialpes.fr/Embedded System Week. [ bib ] |
[18] | Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1--20, 2010. [ bib | DOI | full text on HAL ] |
[17] | Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184--1211, 2010. [ bib | DOI | full text on HAL ] |
[16] | Siegfried M. Rump, Paul Zimmermann, Sylvie Boldo, and Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT, 49(2):419--431, June 2009. [ bib | DOI | full text on HAL ] |
[15] | Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568--589, 2009. [ bib | DOI | full text on HAL | PDF ] |
[14] | Sylvie Boldo, Marc Daumas, and Ren-Cang Li. Formally verified argument reduction with a fused-multiply-add. IEEE Transactions on Computers, 58(8):1139--1145, 2009. [ bib | DOI | PDF | http ] |
[13] | Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4):1--64, 2008. [ bib | DOI ] |
[12] | Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1--2):59--88, 2008. [ bib | full text on HAL | PDF | .pdf ] |
[11] | Louis Mandel and Marc Pouzet. ReactiveML : un langage fonctionnel pour la programmation réactive. Technique et Science Informatiques (TSI), 27(9--10/2008):1097--1128, 2008. [ bib | PDF | .pdf ] |
[10] | Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462--471, 2008. [ bib | DOI | full text on HAL ] |
[9] | Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187--210, 2006. Special Issue of TCS dedicated to a refereed selection of papers presented at TACAS'03. [ bib ] |
[8] | Jean-Christophe Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332--240, 2006. [ bib | DOI | PDF | .pdf ] |
[7] | Alain Girault, Xavier Nicollin, and Marc Pouzet. Automatic Rate Desynchronization of Embedded Reactive Programs. ACM Transactions on Embedded Computing Systems (TECS), 5(3), 2006. [ bib ] |
[6] | Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(1-2):87--106, May 2005. [ bib ] |
[5] | Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325--363, 2005. [ bib | DOI | Abstract ] |
[4] |
Salvador Lucas, Claude Marché, and José Meseguer.
Operational termination of conditional term rewriting systems.
Information Processing Letters, 95:446--453, 2005.
[ bib ]
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs
|
[3] | Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873--897, 2004. [ bib | http ] |
[2] | Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ] |
[1] | Xavier Urbain. Modular and incremental automated termination proofs. Journal of Automated Reasoning, 32:315--355, 2004. [ bib | .ps.gz ] |
Conferences
[305] | Claude Marché and Denis Cousineau. De l'avantage de nuancer les décisions binaires. In 35es Journées Francophones des Langages Applicatifs, 2024. [ bib | full text on HAL ] |
[304] | Amin Timany, Armaël Guéneau, and Lars Birkedal. The logical essence of well-bracketed control flow. In POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages. SIGPLAN, ACM, 2024. [ bib | full text on HAL ] |
[303] | François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével. Thunks and debits in separation logic with time credits. In POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, volume 8. SIGPLAN, ACM, 2024. [ bib | full text on HAL ] |
[302] | Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and Raphaël Rieu-Helft. Formally verified rounding errors of the logarithm-sum-exponential function. In Formal Methods in Computer-Aided Design. IEEE, 2024. [ bib | full text on HAL ] |
[301] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In 25th International Symposium on Formal Methods (FM 2023), volume 14000 of Lecture Notes in Computer Science, pages 39--55, 2023. [ bib | DOI | full text on HAL ] |
[300] | Jean-Christophe 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 274--283, 2023. [ bib | full text on HAL ] |
[299] | Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. In Int. Conf. on Computer Arithmetic, 2023. [ bib | full text on HAL ] |
[298] | Sylvain Conchon and Alexandrina Korneva. The cubicle fuzzy loop: A fuzzing-based extension for the Cubicle model checker. In Carla Ferreira and Tim A. C. Willemse, editors, Software Engineering and Formal Method, volume 14323 of Lecture Notes in Computer Science, pages 30--46. Springer, 2023. [ bib | DOI | full text on HAL ] |
[297] | Léo Andrès, Pierre Chambart, and Jean-Christophe Filliâtre. Wasocaml: compiling OCaml to WebAssembly. In João Saraiva and João Fernandes, editors, 35th Symposium on Implementation and Application of Functional Languages, 2023. [ bib | full text on HAL ] |
[296] | Jean-Christophe 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 ] |
[295] |
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché.
Creusot: a foundry for the deductive verication of Rust programs.
In International Conference on Formal Engineering Methods -
ICFEM, Lecture Notes in Computer Science, Madrid, Spain, 2022. Springer.
[ bib |
full text on HAL ]
Keywords: Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits |
[294] | Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In International Conference on Programming Language Design and Implementation, pages 841--856. ACM, 2022. [ bib | DOI | full text on HAL ] |
[293] | Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. Proving full-system security properties under multiple attacker models on capability machines. In CSF 2022 - 35th IEEE Computer Security Foundations Symposium, 2022. [ bib | full text on HAL ] |
[292] | Léo Andrès, Raja Boujbel, Louis Gesbert, and Dario Pinto. Connecter l'écosystème OCaml à Software Heritage via opam. In Chantal Keller and Timothy Bourke, editors, 33èmes Journées Francophones des Langages Applicatifs, pages 227--234, 2022. [ bib | full text on HAL ] |
[291] | Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Maxime Levillain, Alain Mebsout, and Sylvain Conchon. Jouez à faire consensus avec MITTEN (démonstration). In Chantal Keller and Timothy Bourke, editors, 33èmes Journées Francophones des Langages Applicatifs, pages 248--250, 2022. [ bib | full text on HAL ] |
[290] | Sylvain Conchon. Some insights on open problems in blockchains: Explorative tracks for tezos (invited talk). In Sara Tucci Piergiovanni and Natacha Crooks, editors, 5th International Symposium on Foundations and Applications of Blockchain 2022, FAB 2022, June 3, 2022, Berkeley, CA, USA, volume 101 of OASIcs, pages 2:1--2:1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. [ bib | DOI ] |
[289] | Quentin Garchery. A framework for proof-carrying logical transformations. In Proof eXchange for Theorem Proving, volume 336 of Electronic Proceedings in Theoretical Computer Science, pages 5--23, July 2021. [ bib | DOI | full text on HAL ] |
[288] | Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Explaining counterexamples with giant-step assertion checking. In José Creissac Campos and Andrei Paskevich, editors, 6th Workshop on Formal Integrated Development Environments (F-IDE 2021), Electronic Proceedings in Theoretical Computer Science, May 2021. [ bib | DOI | full text on HAL ] |
[287] |
Jean-Christophe 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.
|
[286] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated verification of temporal properties of Ladder programs. In Formal Methods for Industrial Critical Systems, volume 12863 of Lecture Notes in Computer Science, pages 21--38, 2021. [ bib | DOI | full text on HAL ] |
[285] | Nicolas Osborne and Clément Pascutto. Leveraging formal specifications to generate fuzzing suites. In OCaml Users and Developers Workshop, co-located with the 26th ACM SIGPLAN International Conference on Functional Programming, 2021. [ bib | full text on HAL ] |
[284] | Jean-Christophe 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 ] |
[283] | William Weens, Thibaud Vazquez-Gonzalez, and Louise Ben Salem-Knapp. Modeling round-off errors in hydrodynamic simulations. In 14th International Workshop on Numerical Software Verification, 2021. [ bib | full text on HAL ] |
[282] | Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, volume 195, pages 9:1--9:22, 2021. [ bib | DOI | full text on HAL ] |
[281] | Sylvie Boldo and Guillaume Melquiond. Some formal tools for computer arithmetic: Flocq and Gappa. In Mioara Joldes and Fabrizio Lamberti, editors, 28th IEEE International Symposium on Computer Arithmetic, 2021. [ bib | full text on HAL ] |
[280] | Louise Ben Salem-Knapp, Thibaud Vazquez-Gonzalez, and William Weens. La double précision suffit-elle à l'exascale ? In 20èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, 2021. [ bib | full text on HAL ] |
[279] | Guillaume Melquiond. Plotting in a formally verified way. In 6th Workshop on Formal Integrated Development Environment, volume 338, pages 39--45, 2021. [ bib | DOI | full text on HAL ] |
[278] | Sylvain Conchon, Giorgio Delzanno, and Arnaud Sangnier. Verification of contact tracing protocols via smt-based model checking and counting abstraction. In Stefania Monica and Federico Bergenti, editors, Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, volume 3002 of CEUR Workshop Proceedings, pages 77--91. CEUR-WS.org, 2021. [ bib | .pdf ] |
[277] | Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally documenting tenderbake (short paper). In Bruno Bernardo and Diego Marmsoler, editors, 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference), volume 95 of OASIcs, pages 4:1--4:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [ bib | DOI ] |
[276] | 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. See also https://usr.lmf.cnrs.fr/~jcf/isola-2020/. [ bib | full text on HAL ] |
[275] | 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 ] |
[274] | Diego Diverio, Cláudio Belo Lourenço, and Claude Marché. “You-Know-Why”: an early-stage prototype of a key server developed using Why3. In VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event, pages 4--7, Dublin, Ireland, April 2020. Karlsruhe Institute of Technology. [ bib | DOI | full text on HAL ] |
[273] | Martin Clochard, Claude Marché, and Andrei Paskevich. Deductive verification with ghost monitors. In Principles of Programming Languages, New Orleans, United States, 2020. [ bib | DOI | full text on HAL ] |
[272] | 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://usr.lmf.cnrs.fr/~jcf/hauteur/. [ bib | full text on HAL | Slides ] |
[271] | Quentin Garchery, Chantal Keller, Claude Marché, and Andrei Paskevich. Des transformations logiques passent leur certicat. In Zaynah Dargaye and Yann Régis-Gianas, editors, Trente-et-unièmes Journées Francophones des Langages Applicatifs, Gruissan, France, January 2020. [ bib | full text on HAL ] |
[270] | Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. Analysing installation scenarios of Debian packages. In Tools and Algorithms for the Construction and Analysis of Systems, volume 12079 of Lecture Notes in Computer Science, pages 235--253, 2020. [ bib | DOI | full text on HAL ] |
[269] |
Guillaume Melquiond and Raphaël Rieu-Helft.
WhyMP, a formally verified arbitrary-precision integer library.
In 45th International Symposium on Symbolic and Algebraic
Computation (ISSAC), pages 352--359, 2020.
[ bib |
DOI |
full text on HAL ]
Keywords: Integer arithmetic ; Deductive program verification ; Mathematical library |
[268] |
Sylvie Boldo, Diane Gallois-Wong, and Thibault Hilaire.
A correctly-rounded fixed-point-arithmetic dot-product algorithm.
In 27th IEEE Symposium on Computer Arithmetic (ARITH), pages
9--16. IEEE, 2020.
[ bib |
DOI |
full text on HAL ]
Keywords: Dot Product ; Sum-of-Products ; Correct Round- ing ; Odd Rounding ; Fixed-Point Arithmetic |
[267] |
Thierry Lecomte, David Déharbe, Denis Sabatier, Etienne Prun, Patrick
Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, and Sylvain
Conchon.
Low cost high integrity platform.
In 10th European Congress on Embedded Real Time Systems (ERTS),
Toulouse, France, 2020.
[ bib |
full text on HAL ]
Keywords: Safety ; Certification ; Formal methods |
[266] | Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. In Formal Methods and Software Engineering (ICFEM), pages 55--72, 2020. [ bib | DOI | full text on HAL ] |
[265] | 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 ] |
[264] | Arthur Charguéraud, Jean-Christophe 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 ] |
[263] |
Florian Steinberg, Holger Thies, and Laurent Théry.
Quantitative continuity and Computable Analysis in Coq.
In ITP 2019 - Tenth International Conference on Interactive
Theorem Proving, Portland, United States, September 2019.
The version accepted to the conference can be accessed at
https://drops.dagstuhl.de/opus/volltexte/2019/11083/.
[ bib |
DOI |
full text on HAL ]
Keywords: Computable analysis ; Coq ; Contionuous functionals ; Discontinuity ; Closed choice on the natura |
[262] | Benedikt Becker and Claude Marché. Ghost code in action: Automated verification of a symbolic interpreter. In Supratik Chakraborty and Jorge A.Navas, editors, Verified Software: Tools, Techniques and Experiments, volume 12031 of Lecture Notes in Computer Science, New York, United States, July 2019. [ bib | DOI | full text on HAL ] |
[261] | 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 ] |
[260] | Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root. In Symposium on Computer Arithmetic, pages 183--186, Kyoto, Japan, June 2019. [ bib | full text on HAL ] |
[259] | Florian Faissole. Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. In AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Toulouse, France, June 2019. [ bib | full text on HAL ] |
[258] |
Thibault Hilaire, Hacène Ouzia, and Benoit Lopez.
Optimal Word-Length Allocation for the Fixed-Point Implementation of
Linear Filters and Controllers.
In ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic,
pages 175--182, Kyoto, Japan, June 2019. IEEE.
[ bib |
DOI |
full text on HAL |
.pdf ]
Keywords: fixed-point arithmetic ; word-length allocation |
[257] | Cláudio Belo Lourenço, Maria João Frade, and Jorge Sousa Pinto. A Generalized Program Verification Workflow Based on Loop Elimination and SA Form. In FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, Montreal, Canada, May 2019. [ bib | full text on HAL | .pdf ] |
[256] | Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Second-order linear-time computability with applications to computable analysis. In 15th Annual Conference Theory and Applications of Models of Computation, volume 11436 of Lecture Notes in Computer Science, pages 337--358, Tokyo, Japan, April 2019. Springer. [ bib | full text on HAL ] |
[255] | Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ] |
[254] | Diane Gallois-Wong. Formalisation en Coq d'algorithmes de filtres numériques. In 30èmes Journées Francophones des Langages Applicatifs, January 2019. [ bib | full text on HAL ] |
[253] | 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 ] |
[252] | Valentin Blot, Amina Bousalem, Quentin Garchery, and Chantal Keller. SMTCoq: automatisation expressive et extensible dans Coq. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ] |
[251] | Guillaume Melquiond. Computer arithmetic and formal proofs. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ] |
[250] | Sylvain Conchon and Mattias Roux. Reasoning about universal cubes in MCMT. In Yamine Aït Ameur and Shengchao Qin, editors, International Conference on Formal Engineering Methods, volume 11852 of Lecture Notes in Computer Science, pages 270--285. Springer, 2019. [ bib | full text on HAL ] |
[249] | Guillaume Melquiond and Raphaël Rieu-Helft. A Why3 framework for reflection proofs and its application to GMP's algorithms. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, Oxford, United Kingdom, July 2018. [ bib | full text on HAL ] |
[248] | 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 ] |
[247] | 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 | full text on HAL | .pdf ] |
[246] | Sylvie Boldo, Florian Faissole, and Vincent Tourneur. A formally-proved algorithm to compute the correct average of decimal floating-point numbers. In 25th IEEE Symposium on Computer Arithmetic, Amherst, MA, United States, June 2018. [ bib | full text on HAL ] |
[245] | Pierre Roux, Mohamed Iguernlala, and Sylvain Conchon. A non-linear arithmetic procedure for control-command software verification. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Thessalonique, Greece, April 2018. [ bib | full text on HAL ] |
[244] | Florian Faissole and Bas Spitters. Preuves constructives de programmes probabilistes. 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 ] |
[243] | Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. 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 ] |
[242] | Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour 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 ] |
[241] | 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 ] |
[240] | Sylvain Dailler, Claude Marché, and Yannick Moy. Lightweight interactive proving inside an automatic program verifier. In Proceedings of the Fourth Workshop on Formal Integrated Development Environment, F-IDE, Oxford, UK, July 14, 2018, 2018. [ bib | DOI | full text on HAL ] |
[239] | 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 ] |
[238] | Sylvain Conchon, David Declerck, and Fatiha Zaïdi. Cubicle-w : Parameterized model checking on weak memory. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, International Joint Conference on Automated Reasoning, volume 10900 of Lecture Notes in Computer Science, pages 152--160. Springer, 2018. [ bib | full text on HAL ] |
[237] | Sylvain Conchon, Giorgio Delzanno, and Angelo Ferrando. Declarative parameterized verification of topology-sensitive distributed protocols. In Andreas Podelski and François Taïani, editors, Networked Systems, 6th International Conference, Revised Selected Papers, Lecture Notes in Computer Science, pages 209--224, 2018. [ bib | full text on HAL ] |
[236] | Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
[235] | Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
[234] | Jean-Christophe Filliâtre. Why3 --- where programs meet provers. In KeY Symposium 2017, Rastatt, Germany, October 2017. Invited talk. [ bib ] |
[233] | Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. Formal verification of a floating-point expansion renormalization algorithm. In Proceedings of the 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, September 2017. [ bib | full text on HAL | .pdf ] |
[232] |
Florian Faissole.
Formalization and closedness of finite dimensional subspaces.
In SYNASC 2017 - 19th International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing, Timisoara, Romania, September
2017.
[ bib |
http |
.pdf ]
Keywords: filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq |
[231] | Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error analysis of explicit one-step numerical integration methods. In 24th IEEE Symposium on Computer Arithmetic, London, United Kingdom, July 2017. [ bib | DOI | full text on HAL | .pdf ] |
[230] | Ran Chen and Jean-Jacques Lévy. A semi-automatic proof of strong connectivity. In 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Heidelberg, Germany, July 2017. [ bib | full text on HAL ] |
[229] |
Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond.
How to get an efficient yet verified arbitrary-precision integer
library.
In 9th Working Conference on Verified Software: Theories, Tools,
and Experiments, volume 10712 of Lecture Notes in Computer Science,
pages 84--101, Heidelberg, Germany, July 2017.
[ bib |
DOI |
full text on HAL |
.pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier |
[228] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax--Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ] |
[227] | Jean-Christophe Filliâtre. Why3 tutorial. In VerifyThis 2017, Uppsala, Sweden, April 2017. Invited tutorial. [ bib ] |
[226] | Nicolas Jeannerod. Le coquillage dans le CoLiS-mateur: formalisation d'un langage de programmation de type Shell. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ] |
[225] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ] |
[224] | Ran Chen and Jean-Jacques Lévy. Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
[223] | Martin Clochard. Preuves taillées en biseau. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
[222] | Mário Pereira. Défonctionnaliser pour prouver. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
[221] | Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, and Clément Fumex. A three-tier strategy for reasoning about floating-point numbers in SMT. In Computer Aided Verification, volume 10427 of Lecture Notes in Computer Science, pages 419--435, 2017. [ bib | DOI | full text on HAL ] |
[220] | Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ] |
[219] | Sylvain Conchon, David Declerck, and Fatiha Zaïdi. Compiling parameterized x86-tso concurrent programs to cubicle-w. In Zhenhua Duan and Luke Ong, editors, International Conference on Formal Engineering Methods, number 10610 in Lecture Notes in Computer Science, pages 88--104, 2017. [ bib ] |
[218] | Florian Faissole and Bas Spitters. Synthetic topology in HoTT for probabilistic programming. In The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Paris, France, January 2017. [ bib | full text on HAL ] |
[217] | Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, and Mattias Roux. FAR-Cubicle - A new reachability algorithm for Cubicle. In Daryl Stewart and Georg Weissenbacher, editors, Formal Methods in Computer Aided Design, pages 172--175, 2017. [ bib | DOI | full text on HAL ] |
[216] | Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 9952 of Lecture Notes in Computer Science, pages 461--478, Corfu, Greece, October 2016. Springer. [ bib | DOI | full text on HAL ] |
[215] | Umut A Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski. Dag-calculus: a calculus for parallel computation. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 18--32, Nara, Japan, September 2016. [ bib | DOI | full text on HAL ] |
[214] | Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. In Jasmin Christian Blanchette and Stephan Merz, editors, Proceedings of the 7th International Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, Nancy, France, August 2016. [ bib | DOI | full text on HAL | .pdf ] |
[213] | 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 ] |
[212] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. 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 ] |
[211] | Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. In 9th International Workshop on Numerical Software Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ] |
[210] | Sylvie Boldo. Iterators: where folds fail. In Workshop on High-Consequence Control Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ] |
[209] |
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.
|
[208] | Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché. Specification and proof of high-level functional properties of bit-level programs. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, pages 291--306, Minneapolis, MN, USA, June 2016. Springer. [ bib | full text on HAL ] |
[207] | 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 ] |
[206] | David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Rocco De Nicola and Eva Kühn, editors, Software Engineering and Formal Methods, Lecture Notes in Computer Science, pages 215--233, Vienna, Austria, 2016. [ bib | DOI | full text on HAL ] |
[205] | Arthur Charguéraud. Higher-Order Representation Predicates in Separation Logic. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, Florida, United States, January 2016. [ bib | full text on HAL ] |
[204] | Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, 17th International Conference on Formal Engineering Methods, volume 9407 of Lecture Notes in Computer Science, pages 17--32, Paris, France, November 2015. Springer. [ bib | full text on HAL | .pdf ] |
[203] | Umut A. Acar, Arthur Charguéraud, and Mike Rainey. A Work-Efficient Algorithm for Parallel Unordered Depth-First Search. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ bib | DOI | full text on HAL | http ] |
[202] | Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ bib | DOI | full text on HAL | http ] |
[201] |
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 |
[200] |
Catherine Lelay.
How to express convergence for analysis in Coq.
In The 7th Coq Workshop, Sophia Antipolis, France, June 2015.
[ bib |
full text on HAL ]
Keywords: Coq proof assistant ; Analysis ; Limits ; Filters ; Type-Classes ; Canonical Structures |
[199] | Sylvie Boldo. Stupid is as stupid does: Taking the square root of the square of a floating-point number. In Sergiy Bogomolov and Matthieu Martel, editors, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification, volume 317 of Electronic Notes in Theoretical Computer Science, pages 50--55, Seattle, WA, USA, April 2015. [ bib | DOI | full text on HAL ] |
[198] | Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types. part 2: Local type inference and type reconstruction. In Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, January 2015. ACM Press. [ bib | full text on HAL ] |
[197] | Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib | full text on HAL ] |
[196] | Sylvie Boldo. Formal verification of tricky numerical computations. In 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Würzburg, Germany, September 2014. Invited talk. [ bib | full text on HAL | http ] |
[195] |
Umut A. Acar, Arthur Charguéraud, and Mike Rainey.
Theory and practice of chunked sequences.
In AndreasS. Schulz and Dorothea Wagner, editors, European
Symposium on Algorithms, volume 8737 of Lecture Notes in Computer
Science, pages 25--36, Wroclaw, Poland, September 2014. Springer.
[ bib |
DOI |
full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization |
[194] |
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 |
[193] |
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 |
[192] |
Martin Clochard.
Automatically verified implementation of data structures based on
AVL trees.
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
167--180, Vienna, Austria, July 2014. Springer.
[ bib |
full text on HAL ]
Keywords: Why3 |
[191] |
David Delahaye, Claude Marché, and David Mentré.
Le projet BWare : une plate-forme pour la vérification
automatique d'obligations de preuve B.
In Approches Formelles dans l'Assistance au Développement de
Logiciels (AFADL), Paris, France, June 2014. EasyChair.
[ bib |
full text on HAL ]
Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financé pour 4 ans par le programme Ingénierie Numérique & Sécurité (INS) de l'Agence Nationale de la Recherche (ANR) et a débuté en septembre 2012 (voir le site web du projet : http://bware.lri.fr). Le consortium du projet BWare associe les partenaires académiques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R&D Centre Europe (MERCE), ClearSy, et OCamlPro
|
[190] |
David Delahaye, Catherine Dubois, Claude Marché, and David Mentré.
The BWare project: Building a proof platform for the automated
verification of B proof obligations.
In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume
8477 of Lecture Notes in Computer Science, pages 290--293, Toulouse,
France, June 2014. Springer.
[ bib |
full text on HAL ]
We introduce BWare, an industrial research project that aims to provide a mechanized framework to support the automated veri cation of proof obligations coming from the development of industrial applications using the B method and requiring high integrity. The methodology adopted consists in building a generic verification platform relying on di erent theorem provers, such as rst order provers and SMT (Satisfiability Modulo Theories) solvers. Beyond the multi-tool aspect of our methodology, the originality of this project also resides in the requirement for the veri cation tools to produce proof objects, which are to be checked independently. In this paper, we present some preliminary results of BWare, as well as some current major lines of work
|
[189] | Véronique Benzaken, Évelyne Contejean, and Stefania Dumbrava. A Coq formalization of the relational data model. In Z. Shao, editor, European Symposium on Programming, LNCS 8410, Lecture Notes in Computer Science, pages 189--208, Grenoble, April 2014. Springer. [ bib | full text on HAL ] |
[188] | 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 ] |
[187] | Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages meets Program Verification (PLPV). ACM Press, 2014. [ bib | full text on HAL ] |
[186] | Giuseppe Castagna, Hyeonseung Im, Sergeï Lenglet, Kim Nguyen, Luca Padovani, and Zhiwu Xu. Polymorphic functions with set-theoretic types. part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ] |
[185] | M. Clochard, S. Chaudhuri, and A. Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ] |
[184] | M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ] |
[183] | Sylvain Conchon and Mohamed Iguernelala. Tuning the Alt-Ergo SMT solver for B proof obligations. In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 8477 of Lecture Notes in Computer Science, pages 294--297, Toulouse, France, June 2014. Springer. [ bib | DOI | full text on HAL ] |
[182] | Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib | full text on HAL ] |
[181] | 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://usr.lmf.cnrs.fr/~jcf/publis/bouturage.pdf. [ bib ] |
[180] | Catherine Lelay. Coq passe le bac. In JFLA - Journées francophones des langages applicatifs, Fréjus, France, January 2014. [ bib ] |
[179] |
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Invariants for finite instances and beyond.
In FMCAD, pages 61--68, Portland, Oregon, États-Unis,
October 2013.
[ bib |
DOI |
full text on HAL ]
Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.
|
[178] |
Guillaume Baudart, Florent Jacquemard, Louis Mandel, and Marc Pouzet.
A synchronous embedding of Antescofo, a domain-specific language
for interactive mixed music.
In Thirteen International Conference on Embedded Software
(EMSOFT'13), Montreal, Canada, September 2013.
[ bib |
full text on HAL |
.pdf ]
Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems.
|
[177] |
Guillaume Baudart, Louis Mandel, and Marc Pouzet.
Programming mixed music in ReactiveML.
In ACM SIGPLAN Workshop on Functional Art, Music, Modeling and
Design (FARM'13), Boston, USA, September 2013.
Workshop ICFP 2013.
[ bib |
full text on HAL |
.pdf ]
Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesized sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming.
|
[176] |
Louis Mandel, Cédric Pasteur, and Marc Pouzet.
Time refinement in a functional synchronous language.
In Proceedings of 15th ACM SIGPLAN International Symposium on
Principles and Practice of Declarative Programming (PPDP'13), Madrid,
Spain, September 2013.
[ bib |
full text on HAL |
.pdf ]
Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.
|
[175] | Catherine Lelay. A New Formalization of Power Series in Coq. In 5th Coq Workshop, pages 1--2, Rennes, France, July 2013. http://coq.inria.fr/coq-workshop/2013#Lelay. [ bib | full text on HAL ] |
[174] | Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, Lake Placid, USA, June 2013. Springer. [ bib | full text on HAL | .pdf ] |
[173] |
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 |
[172] |
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 |
[171] | Jean-Christophe Filliâtre. Deductive program verification with Why3. In MSR-Inria Joint Centre “Spring Day”, Lyon, France, May 2013. Invited talk. [ bib ] |
[170] |
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 |
[169] | Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 41--60. Springer, March 2013. [ bib | full text on HAL ] |
[168] | Claude Marché and Asma Tafat. Calcul de plus faible précondition, revisité en Why3. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ] |
[167] | Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ] |
[166] | 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. https://github.com/backtracking/combine/. [ bib | full text on HAL | http ] |
[165] |
Louis Mandel and Cédric Pasteur.
Réactivité des systèmes coopératifs : le cas de
ReactiveML.
In Vingt-quatrièmes Journées Francophones des Langages
Applicatifs, Aussois, France, February 2013.
http://rml.lri.fr/jfla13.
[ bib |
full text on HAL |
.pdf ]
La concurrence coopérative est un modèle de programmation très répandu. On peut par exemple l'utiliser en OCaml à travers des bibliothèques comme Lwt, Async ou Equeue. Il a de nombreux avantages tels que l'absence de courses critiques et des implantations légères et efficaces. Néanmoins, un des inconvénients majeurs de ce modèle est qu'il dépend de la discipline du programmeur pour garantir que le système est réactif : un processus peut empêcher les autres de s'exécuter.
|
[164] | Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Scheduling parallel programs by work stealing with private deques. In Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, PPoPP '13, pages 219--228. ACM Press, February 2013. [ bib | DOI | full text on HAL ] |
[163] | Véronique Benzaken, Giuseppe Castagna, Kim Nguyen, and Jérôme Siméon. Static and dynamic semantics of NoSQL languages. In R. Cousot, editor, Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Roma, Italy, January 2013. ACM Press. [ bib | full text on HAL ] |
[162] | Sylvie Boldo. How to compute the area of a triangle: a formal revisit. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ] |
[161] | Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ] |
[160] | 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 ] |
[159] | Daisuke Ishii, Guillaume Melquiond, and Shin Nakajima. Inductive verification of hybrid automata with strongest postcondition calculus. In Einar Broch Johnsen and Luigia Petre, editors, Proceedings of the 10th Conference on Integrated Formal Methods, volume 7940 of Lecture Notes in Computer Science, pages 139--153, Turku, Finland, 2013. [ bib | DOI | full text on HAL ] |
[158] | Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A collaborative framework for non-linear integer arithmetic reasoning in alt-ergo. In 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 161--168, 2013. [ bib | DOI ] |
[157] | Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, December 2012. [ bib | DOI | full text on HAL ] |
[156] |
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 |
http ]
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.
|
[155] |
Vijay Saraswat, David Cunningham, Liana Hadarean, Louis Mandel, Avraham
Shinnar, and Olivier Tardieu.
Constrained types - future directions.
In 18th International Conference on Principles and Practice of
Constraint Programming, Québec City, Canada, October 2012.
Position Paper.
[ bib |
full text on HAL |
.pdf ]
The use of constraints in types is quite natural. Yet, integrating constraint based types into the heart of a modern, statically typed, object-oriented programming language is quite tricky. Over the last five years we have designed and implemented the constrained types framework in the programming language X10. In this paper we review the conceptual design, the practical implementation issues, and the many new questions that are raised. We expect the pursuit of these questions to be a profitable area of future work.
|
[154] |
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 |
[153] |
David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine
Paulin-Mohring.
Towards Provably Robust Watermarking.
In ITP 2012, volume 7406 of Lecture Notes in Computer
Science, August 2012.
[ bib |
full text on HAL |
.pdf ]
Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking. Keywords: watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving |
[152] | 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 ] |
[151] |
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Cubicle: A parallel SMT-based model checker for parameterized
systems.
In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV
2012: Proceedings of the 24th International Conference on Computer Aided
Verification, volume 7358 of Lecture Notes in Computer Science,
Berkeley, California, USA, July 2012. Springer.
[ bib |
full text on HAL ]
Cubicle is a new model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show that Cubicle is effective and competitive with state-of-the-art model checkers.
|
[150] |
Louis Mandel and Florence Plateau.
Scheduling and buffer sizing of n-synchronous systems: Typing of
ultimately periodic clocks in Lucy-n.
In Eleventh International Conference on Mathematics of Program
Construction (MPC'12), Madrid, Spain, June 2012.
[ bib |
.pdf ]
Lucy-n is a language for programming networks of processes communicating through bounded buffers. A dedicated type system, termed a clock calculus, automatically computes static schedules of the processes and the sizes of the buffers between them.
|
[149] |
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.
|
[148] |
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplex-based extension of Fourier-Motzkin for solving linear
integer arithmetic.
In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors,
IJCAR 2012: Proceedings of the 6th International Joint Conference on
Automated Reasoning, volume 7364 of Lecture Notes in Computer Science,
pages 67--81, Manchester, UK, June 2012. Springer.
[ bib |
DOI |
full text on HAL ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.
|
[147] |
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.
|
[146] | 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 ] |
[145] | Catherine Lelay and Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. In Vingt-troisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012. [ bib | full text on HAL ] |
[144] | Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 2--17, Philadelphia, USA, January 2012. Springer. [ bib | full text on HAL | .pdf ] |
[143] |
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 |
[142] | 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 ] |
[141] | Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Built-in treatment of an axiomatic floating-point theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, pages 12--21, Manchester, UK, 2012. LORIA. [ bib ] |
[140] | Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. LORIA. [ bib ] |
[139] | Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium on Formal Methods, volume 7436 of Lecture Notes in Computer Science, pages 147--154. Springer, 2012. [ bib | full text on HAL ] |
[138] | Denis Cousineau and Olivier Hermant. A semantic proof that reducibility candidates entail cut elimination. In Ashish Tiwari, editor, 23nd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics, pages 133--148, Nagoya, Japan, 2012. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL ] |
[137] | Johannes Kanig, Edmond Schonberg, and Claire Dross. Hi-Lite: the convergence of compiler technology and program verification. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pages 27--34, Boston, USA, 2012. ACM Press. [ bib ] |
[136] | Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science, pages 314--329. Springer, December 2011. [ bib | full text on HAL ] |
[135] |
Louis Mandel, Florence Plateau, and Marc Pouzet.
Static scheduling of latency insensitive designs with Lucy-n.
In Formal Methods in Computer Aided Design (FMCAD 2011),
Austin, TX, USA, October 2011.
[ bib |
full text on HAL |
.pdf ]
Lucy-n is a dataflow programming language similar to Lustre extended with a buffer operator. This language is based on the n-synchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucy-n is also applicable to model Latency Insensitive Designs (LID). In order to model relay stations, we have to introduce a delay operator. Thanks to this new operator, a LID can be described by a Lucy-n program. Then, the Lucy-n compiler automatically provides static schedules for computation nodes and buffer sizes needed in the shell wrappers.
|
[134] | François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 87--102, Saarbrücken, Germany, October 2011. [ bib | .pdf ] |
[133] |
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 |
[132] |
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.
|
[131] |
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.
|
[130] | Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of Lecture Notes in Computer Science, pages 45--59, Saarbrücken, Germany, April 2011. Springer. [ bib | DOI | full text on HAL | .pdf | Abstract ] |
[129] |
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet.
Divide and recycle: types and compilation for a hybrid synchronous
language.
In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools
and Theory for Embedded Systems (LCTES'11), Chicago, USA, April 2011.
[ bib |
.pdf ]
Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.
|
[128] | Véronique Benzaken, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib | full text on HAL ] |
[127] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In Manfred Schmidt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics, pages 21--30, Novi Sad, Serbia, 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL | http | Abstract ] |
[126] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153--167. Springer, January 2011. [ bib | full text on HAL ] |
[125] | Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ] |
[124] | 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 ] |
[123] |
Louis Mandel and Florence Plateau.
Typage des horloges périodiques en Lucy-n.
In Sylvain Conchon, editor, Vingt-deuxièmes Journées
Francophones des Langages Applicatifs, La Bresse, France, January 2011.
INRIA.
[ bib |
.pdf ]
Lucy-n est un langage permettant de programmer des réseaux de processus communiquant à travers des buffers de taille bornée. La taille des buffers et les rythmes d'exécution relatifs des processus sont calculés par une phase de typage appelée calcul d'horloge. Ce typage nécessite la résolution d'un ensemble de contraintes de sous-typage. L'an dernier, nous avons proposé un algorithme de résolution de ces contraintes utilisant des méthodes issues de l'interprétation abstraite. Cette année nous présentons un algorithme tirant profit de toute l'information contenue dans les types.
|
[122] | Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, 2011. [ bib | DOI | full text on HAL ] |
[121] | David Baelde, Romain Beauxis, and Samuel Mimram. Liquidsoap: A high-level programming language for multimedia streaming. In Ivana Cerná, Tibor Gyimóthy, Juraj Hromkovic, Keith G. Jeffery, Rastislav Královic, Marko Vukolic, and Stefan Wolf, editors, 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11), volume 6543 of Lecture Notes in Computer Science, Nový Smokovec, Slovakia, January 2011. Springer. [ bib ] |
[120] | Véronique Benzaken, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib ] |
[119] | Albert Benveniste, Benoit Caillaud, and Marc Pouzet. The Fundamentals of Hybrid Systems Modelers. In 49th IEEE International Conference on Decision and Control (CDC), Atlanta, Georgia, USA, December 15-17 2010. [ bib ] |
[118] | Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Andrei Voronkov, editor, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, Yogyakarta, Indonesia, October 2010. (short paper). [ bib ] |
[117] | 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 ] |
[116] | Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 127--141, Edinburgh, Scotland, July 2010. Springer. [ bib | full text on HAL ] |
[115] | Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. In Proceedings of the Third International Workshop on Numerical Software Verification, Edinburgh, Scotland, July 2010. NSV-8. [ bib | full text on HAL ] |
[114] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pages 143--159, Paris, France, June 2010. http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083. [ bib | full text on HAL ] |
[113] |
Louis Mandel, Florence Plateau, and Marc Pouzet.
Lucy-n: a n-synchronous extension of Lustre.
In Tenth International Conference on Mathematics of Program
Construction (MPC 2010), Québec, Canada, June 2010.
[ bib |
.pdf ]
Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The n-synchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compile-time. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.
|
[112] | Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14--23, Washington D.C., USA, April 2010. [ bib | full text on HAL | PDF ] |
[111] | Louis Mandel, Florence Plateau, and Marc Pouzet. Clock typing of n-synchronous programs. In Designing Correct Circuits (DCC 2010), Paphos, Cyprus, March 2010. [ bib ] |
[110] | Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n : une extension n-synchrone de Lustre. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ] |
[109] | Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani Kalyanasundaram, and Marco Roveri. Tighter integration of BDDs and SMT for predicate abstraction. In Design, Automation & Test in Europe, Dresden. Germany, March 2010. IEEE. [ bib | full text on HAL ] |
[108] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ] |
[107] | Sebastian Maneth and Kim Nguyen. Xpath whole query optimization. In 36th International Conference on Very Large Data Bases (VLDB'2010), volume 3, pages 882--893, 2010. [ bib ] |
[106] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In John P. Gallagher and Janis Voigtländer, editors, Partial Evaluation and Program Manipulation, pages 63--72, Madrid, Spain, January 2010. ACM Press. [ bib | DOI | Abstract ] |
[105] | 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 ] |
[104] |
Louis Mandel, Florence Plateau, and Marc Pouzet.
Lucy-n : une extension n-synchrone de Lustre.
In Vingt-et-unièmes Journées Francophones des Langages
Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA.
[ bib |
.pdf ]
Les langages synchrones flot de données permettent de programmer des réseaux de processus communicant sans buffers. Pour cela, chaque flot est associé à un type d'horloges, qui indique les instants de présence de valeurs sur le flot. La communication entre deux processus f et g peut être faite sans buffer si le type du flot de sortie de f est égal au type du flot d'entrée de g. Un système de type, le calcul d'horloge, infère des types tels que cette condition est vérifiée. Le modèle n-synchrone a pour but de relâcher ce modèle de programmation en autorisant les communications à travers des buffers de taille bornée. En pratique, cela consiste à introduire une règle de sous-typage dans le calcul d'horloge.
|
[103] | Louis Mandel. Cours de ReactiveML. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ] |
[102] | Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Specifying generic Java programs: two case studies. In Claus Brabrand and Pierre-Etienne Moreau, editors, Tenth Workshop on Language Descriptions, Tools and Applications. ACM Press, 2010. [ bib | full text on HAL ] |
[101] | 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 Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 147--162. Springer, 2010. [ bib | DOI | full text on HAL ] |
[100] | Paolo Herms. Certification of a chain for deductive program verification. In Yves Bertot, editor, 2nd Coq Workshop, satellite of ITP'10, 2010. [ bib | full text on HAL ] |
[99] | Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks: An efficient symbolic representation. In ACM International Conference on Embedded Software (EMSOFT'09), Grenoble, France, October 2009. [ bib ] |
[98] | Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks: An efficient symbolic representation. In ACM International Conference on Embedded Software (EMSOFT'09), Grenoble, France, October 2009. [ bib ] |
[97] | Stéphane Lescuyer and Sylvain Conchon. Improving Coq propositional reasoning using a lazy CNF conversion scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287--303, Trento, Italy, September 2009. Springer. [ bib | DOI ] |
[96] |
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.
|
[95] | Louis Mandel, Florence Plateau, and Marc Pouzet. The ReactiveML toplevel (tool demonstration). In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [ bib ] |
[94] | 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 ] |
[93] |
Clément Hurlin, François Bobot, and Alexander J. Summers.
Size does matter : Two certified abstractions to disprove entailment
in intuitionistic and classical separation logic.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming (IWACO'09), July 2009.
Coq proofs:
http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz.
[ bib |
full text on HAL |
.pdf ]
We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A does not entail B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).
|
[92] | Paul Caspi, Jean-Louis Colaço, Léonard Gérard, Marc Pouzet, and Pascal Raymond. Synchronous Objects with Scheduling Policies: Introducing safe shared memory in Lustre. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Dublin, June 2009. [ bib ] |
[91] | Paul Caspi, Jean-Louis Colaço, Léonard Gérard, Marc Pouzet, and Pascal Raymond. Synchronous Objects with Scheduling Policies: Introducing safe shared memory in Lustre. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Dublin, June 2009. [ bib ] |
[90] | Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Relaxing synchronous composition with clock abstraction. In Hardware Design using Functional languages (HFL 09), pages 35--52, York, UK, March 2009. [ bib ] |
[89] | 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 ] |
[88] |
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 LATEX dans les figures. Ocaml offre une alternative séduisante aux langages de macros LATEX, 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.
|
[87] |
Louis Mandel and Florence Plateau.
Abstraction d'horloges dans les systèmes synchrones flot de
données.
In Vingtièmes Journées Francophones des Langages
Applicatifs, Saint-Quentin sur Isère, January 2009. INRIA.
[ bib |
.pdf ]
Les langages synchrones flot de données tels que Lustre manipulent des séquences infinies de données comme valeurs de base. Chaque flot est associé à une horloge qui définit les instants où sa valeur est présente. Cette horloge est une information de type et un système de types dédié, le calcul d'horloges, rejette statiquement les programmes qui ne peuvent pas être exécutés de manière synchrone. Dans les langages synchrones existants, cela revient à se demander si deux flots ont la même horloge et repose donc uniquement sur l'égalité d'horloges. Des travaux récents ont montré l'intérêt d'introduire une notion relâchée du synchronisme, où deux flots peuvent être composés dès qu'ils peuvent être synchronisés par l'introduction d'un buffer de taille bornée (comme c'est fait dans le modèle SDF d'Edward Lee). Techniquement, cela consiste à remplacer le typage par du sous-typage. Ce papier est une traduction et amélioration technique de [84] qui présente un moyen simple de mettre en oeuvre ce modèle relâché par l'utilisation d'horloges abstraites. Les valeurs abstraites représentent des ensembles d'horloges concrètes qui ne sont pas nécessairement périodiques. Cela permet de modéliser divers aspects des logiciels temps-réel embarqués, tels que la gigue bornée présente dans les systèmes vidéo, le temps d'exécution des processus temps réel et, plus généralement, la communication à travers des buffers de taille bornée. Nous présentons ici l'algèbre des horloges abstraites et leurs principales propriétés théoriques.
|
[86] | Sylvie Boldo. Floats and ropes: A case study for formal numerical program verification. In 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science, pages 91--102. Springer, 2009. [ bib | DOI ] |
[85] | William Edmonson and Guillaume Melquiond. IEEE interval standard working group - P1788: current status. In Javier D. Bruguera, Marius Cornea, Debjit DasSarma, and John Harrison, editors, Proceedings of the 19th IEEE Symposium on Computer Arithmetic, pages 231--234, Portland, OR, USA, 2009. [ bib | DOI ] |
[84] |
Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet.
Abstraction of Clocks in Synchronous Data-flow Systems.
In The Sixth ASIAN Symposium on Programming Languages and
Systems (APLAS), volume 5356 of Lecture Notes in Computer Science,
pages 237--254, Bangalore, India, December 2008.
[ bib |
PDF |
.pdf ]
Synchronous data-flow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system --- the so-called clock-calculus --- statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by subtyping. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are sets of concrete clocks which are not necessarily periodic. This allows to model various features in real-time embedded software such as bounded jitter as found in video-systems, execution time of real-time processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.
|
[83] |
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.
|
[82] |
Matthieu Sozeau and Nicolas Oury.
First-Class Type Classes.
In Otmame Aït-Mohamed, César Muñoz, and Sofiène Tahar,
editors, 21th International Conference on Theorem Proving in Higher
Order Logics, volume 5170 of Lecture Notes in Computer Science.
Springer, August 2008.
[ bib |
Slides |
.pdf ]
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.
|
[81] | V. Benzaken, G.Castagna, D. Colazzo, and C. Miachon. Pattern by example: Type-driven visual programming of XML queries". In 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, Valencia, Spain, July 2008. ACM Press. [ bib ] |
[80] | Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. In Marc Daumas and Javier Bruguera, editors, Proceedings of the 8th Conference on Real Numbers and Computers, pages 113--122, Santiago de Compostela, Spain, July 2008. [ bib | full text on HAL | PDF ] |
[79] | Romain Bardou. Ownership, pointer arithmetic and memory separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib | .pdf ] |
[78] | Gwenael Delaval, Alain Girault, and Marc Pouzet. A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ] |
[77] | Dariusz Biernacki, Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Clock-directed Modular Code Generation of Synchronous Data-flow Languages. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ] |
[76] | Évelyne Contejean and Xavier Urbain. The A3PAT approach. In Workshop on Certified Termination WScT08, Leipzig, Germany, May 2008. [ bib ] |
[75] | Sylvain Conchon and Jean-Christophe Filliâtre. Semi-persistent data structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | DOI | full text on HAL | PDF ] |
[74] | Louis Mandel and Florence Plateau. Interactive programming of reactive systems. In Proceedings of Model-driven High-level Programming of Embedded Systems (SLA++P'08), Electronic Notes in Computer Science, pages 44--59, Budapest, Hungary, April 2008. Elsevier Science Publishers. [ bib | PDF | .pdf ] |
[73] | Évelyne Contejean. Coccinelle, a Coq library for rewriting. In Types, Torino, Italy, March 2008. [ bib ] |
[72] | Giuseppe Castagna and Kim Nguyen. Typed iterators for XML. In James Hook and Peter Thiemann, editors, ICFP, pages 15--26, Victoria, BC, Canada, September 2008. ACM. [ bib ] |
[71] | François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1--5, 2008. [ bib | DOI | PDF | .pdf | Abstract ] |
[70] |
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
theories.
In Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198(2) of
Electronic Notes in Computer Science, pages 51--69. Elsevier Science
Publishers, 2008.
[ bib |
DOI ]
We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantical values for class representatives instead of canonized terms. Using semantical values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.
|
[69] |
Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer.
SAT-MICRO : petit mais costaud !
In Dix-neuvièmes Journées Francophones des Langages
Applicatifs, Étretat, France, January 2008. INRIA.
[ bib |
.ps ]
Le problème SAT, qui consiste `a déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en Ocaml d'un SAT-solver, baptisé SAT-MICRO, intégrant ces optimisations. Le fonctionnement de SAT-MICRO est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.
|
[68] |
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.
|
[67] | Louis Mandel and Luc Maranget. Programming in JoCaml (tool demonstration). In 17th European Symposium on Programming (ESOP'08), pages 108--111, Budapest, Hungary, April 2008. [ bib | PDF | .pdf ] |
[66] | 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 ] |
[65] | Yannick Moy. Sufficient preconditions for modular assertion checking. In Francesco Logozzo, Doron Peled, and Lenore Zuck, editors, 9th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 4905 of Lecture Notes in Computer Science, pages 188--202, San Francisco, California, USA, January 2008. Springer. [ bib | PDF | .pdf ] |
[64] | Stéphane Lescuyer and Sylvain Conchon. A reflexive formalization of a SAT solver in Coq. In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008. [ bib ] |
[63] |
Yann Régis-Gianas and François Pottier.
A Hoare logic for call-by-value functional programs.
In Proceedings of the Ninth International Conference on
Mathematics of Program Construction (MPC'08), pages 305--335, 2008.
[ bib |
DOI |
.pdf ]
We present a Hoare logic for a call-by-value programming language equipped with recursive, higher-order functions, algebraic data types, and a polymorphic type system in the style of Hindley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions. These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactive theorem provers. Although the technical apparatus that we exploit is by now standard, its application to functional programming languages appears to be new, and (we claim) deserves attention. As a sample application, we check the partial correctness of a balanced binary search tree implementation.
|
[62] | Dariusz Biernacki, Jean-Louis Colaço, and Marc Pouzet. Clock-directed Modular Code Generation from Synchronous Block Diagrams. In Workshop on Automatic Program Generation for Embedded Systems (APGES 2007), Salzburg, Austria, October 2007. [ bib | PDF | .pdf ] |
[61] |
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.
|
[60] |
Jean-Christophe Filliâtre.
Formal Verification of MIX Programs.
In Journées en l'honneur de Donald E. Knuth, Bordeaux,
France, October 2007.
[ 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.
|
[59] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 148--162, Liverpool,UK, September 2007. Springer. [ bib | DOI | Abstract ] |
[58] |
Jean-François Couchot and Thierry Hubert.
A Graph-based Strategy for the Selection of Hypotheses.
In FTP 2007 - International Workshop on First-Order Theorem
Proving, Liverpool, UK, September 2007.
[ bib |
PDF |
.pdf ]
In previous works on verifying C programs by deductive approaches based on SMT provers, we proposed the heuristic of separation analysis to handle the most difficult problems. Nevertheless, this heuristic is not sufficient when applied on industrial C programs: it remains some Verification Conditions (VCs) that cannot be decided by any SMT prover, mainly due to their size. This work presents a strategy to select relevant hypotheses in each VC. The relevance of an hypothesis is the combination of two separated dependency analysis obtained by some graph traversals. The approach is applied on a benchmark issued from an industrial program verification.
|
[57] |
Jean-François Couchot and Stéphane Lescuyer.
Handling polymorphism in automated deduction.
In 21th International Conference on Automated Deduction
(CADE-21), volume 4603 of LNCS (LNAI), pages 263--278, Bremen,
Germany, July 2007.
[ bib |
PDF |
.pdf ]
Polymorphism has become a common way of designing short and reusable programs by abstracting generic definitions from type-specific ones. Such a convenience is valuable in logic as well, because it unburdens the specifier from writing redundant declarations of logical symbols. However, top shelf automated theorem provers such as Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To this end, we present efficient reductions of polymorphism in both unsorted and many-sorted first order logics. For each encoding, we show that the formulas and their encoded counterparts are logically equivalent in the context of automated theorem proving. The efficiency keynote is to disturb the prover as little as possible, especially the internal decision procedures used for special sorts, e.g. integer linear arithmetic, to which we apply a special treatment. The corresponding implementations are presented in the framework of the Why/Caduceus toolkit.
|
[56] |
Jean-François Couchot and Frédéric Dadeau.
Guiding the correction of parameterized specifications.
In Integrated Formal Methods, volume 4591 of Lecture Notes
in Computer Science, pages 176--194, Oxford, UK, July 2007. Springer.
[ bib |
PDF |
.pdf ]
Finding inductive invariants is a key issue in many domains such as program verification, model based testing, etc. However, few approaches help the designer in the task of writing a correct and meaningful model, where correction is used for consistency of the formal specification w.r.t. its inner invariant properties. Meaningfulness is obtained by providing many explicit views of the model, like animation, counter-example extraction, and so on. We propose to ease the task of writing a correct and meaningful formal specification by combining a panel of provers, a set-theoretical constraint solver and some model-checkers.
|
[55] | 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 ] |
[54] | Yannick Moy. Union and cast in deductive verification. In Proceedings of the C/C++ Verification Workshop, volume Technical Report ICIS-R07015, pages 1--16. Radboud University Nijmegen, July 2007. [ bib | PDF | .pdf ] |
[53] | Malgorzata Biernacka and Dariusz Biernacki. Formalizing Constructions of Abstract Machines for Functional Languages in Coq. In 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), pages 84--99, Paris, France, June 2007. [ bib | PDF | .pdf ] |
[52] | Claude Marché and Hans Zantema. The termination competition. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications (RTA'07), volume 4533 of Lecture Notes in Computer Science, pages 303--313, Paris, France, June 2007. Springer. [ bib | Slides | PDF | .pdf ] |
[51] | Claude Marché, Hans Zantema, and Johannes Waldmann. The termination competition 2007. In Dieter Hofbauer and Alexander Serebrenik, editors, Extended Abstracts of the 9th International Workshop on Termination, WST'07, June 2007. http://www.lri.fr/~marche/termination-competition/. [ bib | http ] |
[50] |
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.
|
[49] | 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 ] |
[48] | Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), pages 81--93, Braga, Portugal, March 2007. [ bib | full text on HAL ] |
[47] | Lionel Morel and Louis Mandel. Executable contracts for incremental prototypes of embedded systems. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA'07), pages 123--136. Elsevier Science Publishers, March 2007. [ bib | PDF | .pdf ] |
[46] | Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), pages 35--51, Braga, Portugal, March 2007. [ bib | PDF | .pdf ] |
[45] |
Sylvie Boldo and Jean-Christophe Filliâtre.
Formal verification of floating-point programs.
In 18th IEEE International Symposium on Computer Arithmetic,
pages 187--194, 2007.
[ bib |
DOI |
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.
|
[44] |
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane
Lescuyer.
Lightweight Integration of the Ergo Theorem Prover inside a Proof
Assistant.
In John Rushby and N. Shankar, editors, Proceedings of the
second workshop on Automated formal methods, pages 55--59. ACM Press, 2007.
[ bib |
DOI |
PDF |
.pdf ]
Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.
|
[43] | Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. CC(X): Efficiently combining equality and solvable theories without canonizers. In Sava Krstic and Albert Oliveras, editors, SMT 2007: 5th International Workshop on Satisfiability Modulo, 2007. [ bib ] |
[42] |
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.
|
[41] | Sébastien Labbé, Jean-Pierre Gallois, and Marc Pouzet. Slicing communicating automata specifications for efficient model reduction. In 18th Australian Conference on Software Engineering (ASWEC), 2007. [ bib ] |
[40] | Claude Marché. Jessie: an intermediate language for Java and C verification. In Programming Languages meets Program Verification (PLPV), pages 1--2, Freiburg, Germany, 2007. ACM Press. [ bib | DOI ] |
[39] |
Matthieu Sozeau.
Subset coercions in Coq.
In Thorsten Altenkirch and Conor Mc Bride, editors, Types for
Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK,
April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture
Notes in Computer Science, pages 237--252. Springer, 2007.
[ bib |
Slides |
.pdf ]
We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “Predicate subtyping” feature of PVS and following mathematical convention. The typing judgements can be translated to the Calculus of Inductive Constructions by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.
|
[38] |
Matthieu Sozeau.
Program-ing finger trees in Coq.
In Ralf Hinze and Norman Ramsey, editors, 12th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2007, pages 13--24,
Freiburg, Germany, 2007. ACM Press.
[ bib |
DOI |
Slides |
.pdf ]
Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent data structure with good performance. Their genericity permits developing a wealth of structures like ordered sequences or interval trees on top of a single implementation. However, the type systems used by current functional languages do not guarantee the coherent parameterization and specialization of Finger Trees, let alone the correctness of their implementation. We present a certified implementation of Finger Trees solving these problems using the Program extension of Coq. We not only implement the structure but also prove its invariants along the way, which permit building certified structures on top of Finger Trees in an elegant way.
|
[37] | Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Mixing Signals and Modes in Synchronous Data-flow Systems. In ACM International Conference on Embedded Software (EMSOFT'06), Seoul, South Korea, October 2006. [ bib ] |
[36] | 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 ] |
[35] | Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ] |
[34] | Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. IEEE Comp. Soc. Press. [ bib ] |
[33] | Sylvie Boldo. Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms. In Ulrich Furbach and Natarajan Shankar, editors, Third International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 52--66, Seattle, USA, August 2006. Springer. [ bib | PDF | .pdf ] |
[32] | Nicolas Halbwachs and Louis Mandel. Simulation and verification of asynchronous systems by means of a synchronous model. In Sixth International Conference on Application of Concurrency to System Design (ACSD'06), pages 3--14, Turku, Finland, June 2006. [ bib | PDF | .pdf ] |
[31] | Ludovic Samper, Florence Maraninchi, Laurent Mounier, and Louis Mandel. GLONEMO: Global and accurate formal models for the analysis of ad hoc sensor networks. In Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06), Nice, France, May 2006. ACM Press. [ bib | PDF | .pdf ] |
[30] | Sylvie Boldo and César Muñoz. Provably faithful evaluation of polynomials. In Proceedings of the 21st Annual ACM Symposium on Applied Computing, volume 2, pages 1328--1332, Dijon, France, April 2006. [ bib | full text on HAL ] |
[29] | June Andronick and Boutheina Chetali. An Environment for Securing Smart Cards Embedded C Code. In International Conference on Research in Smart Cards (Esmart'06), 2006. [ bib ] |
[28] | Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. In Tarmo Uustalu, editor, Mathematics of Program Construction, MPC 2006, volume 4014 of Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer. [ bib | PDF | .pdf ] |
[27] | Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs. INRIA, January 2006. [ bib | .ps.gz ] |
[26] | Claude Marché and Hans Zantema. The termination competition 2006. In Alfons Geser and Harald Sondergaard, editors, Extended Abstracts of the 8th International Workshop on Termination, WST'06, August 2006. http://www.lri.fr/~marche/termination-competition/. [ bib | http ] |
[25] | Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06) [24]. [ bib ] |
[24] | Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006. [ bib ] |
[23] | Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib | http ] |
[22] | Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ] |
[21] | Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05) [20]. [ bib ] |
[20] | Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ] |
[19] | Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ] |
[18] | Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179--194. Springer, August 2005. [ bib | .ps ] |
[17] | Nicolas Oury. Extensionality in the Calculus of Constructions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 278--293. Springer, August 2005. [ bib ] |
[16] | June Andronick, Boutheina Chetali, and Christine Paulin-Mohring. Formal verification of security properties of smart card embedded source code. In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, International Symposium of Formal Methods Europe (FM'05), volume 3582 of Lecture Notes in Computer Science, Newcastle,UK, July 2005. Springer. [ bib ] |
[15] | Évelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In Robert Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Artificial Intelligence, pages 7--22, Tallinn, Estonia, July 2005. Springer. [ bib | DOI | Abstract ] |
[14] | Louis Mandel and Marc Pouzet. ReactiveML, a Reactive Extension to ML. In ACM International Conference on Principles and Practice of Declarative Programming (PPDP), pages 82--93, Lisboa, July 2005. [ bib | PDF | .pdf ] |
[13] | Louis Mandel and Farid Benbadis. Simulation of mobile ad hoc network protocols in ReactiveML. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP'05), Edinburgh, Scotland, April 2005. Elsevier Science Publishers. [ bib | PDF | .pdf ] |
[12] | 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 ] |
[11] | Pierre Corbineau. Skip lists et arbres binaires de recherche probabilistes. In Seizièmes Journées Francophones des Langages Applicatifs, pages 99--112. INRIA, March 2005. [ bib ] |
[10] | Louis Mandel and Marc Pouzet. ReactiveML, un langage pour la programmation réactive en ML. In Seizièmes Journées Francophones des Langages Applicatifs, pages 1--16. INRIA, March 2005. [ bib | .ps ] |
[9] | Julien Signoles. Une approche fonctionnelle du modèle vue-contrôleur. In Seizièmes Journées Francophones des Langages Applicatifs, pages 63--78. INRIA, March 2005. [ bib ] |
[8] | G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In R. Gorrieri, F. Martinelli, P. Ryan, and S. Schneider, editors, Proceedings of FAST'05, volume 3866 of Lecture Notes in Computer Science, pages 112--126. Springer, 2005. [ bib ] |
[7] | Sylvie Boldo and Jean-Michel Muller. Some functions computable with a fused-mac. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th Symposium on Computer Arithmetic, pages 52--58, Cape Cod, USA, 2005. [ bib | .pdf ] |
[6] | Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ] |
[5] | 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 ] |
[4] | Bart Jacobs, Claude Marché, and Nicole Rauch. Formal verification of a commercial smart card applet with multiple tools. In Algebraic Methodology and Software Technology, volume 3116 of Lecture Notes in Computer Science, Stirling, UK, July 2004. Springer. [ bib ] |
[3] | Évelyne Contejean. A certified AC matching algorithm. In Vincent van Oostrom, editor, 15th International Conference on Rewriting Techniques and Applications, volume 3091 of Lecture Notes in Computer Science, pages 70--84, Aachen, Germany, June 2004. Springer. [ bib | DOI | Abstract ] |
[2] | Pierre Corbineau. First-order reasoning in the Calculus of Inductive Constructions. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES 2003 : Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 162--177, Torino, Italy, April 2004. Springer. [ bib | .ps | .ps ] |
[1] | 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 ] |
PhD theses
[45] | Clément Pascutto. Runtime Verification of OCaml Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib ] |
[44] | Xavier Denis. Deductive Verification of Rust Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib | full text on HAL ] |
[43] | Antoine Lanco. Stratégies pour la réduction forte. Phd thesis, Université Paris-Saclay, 2023. [ bib | full text on HAL ] |
[42] | Quentin Garchery. Certification de la transformation de tâches de preuve. Thèse de doctorat, Université Paris-Saclay, 2022. [ bib | full text on HAL ] |
[41] | Diane Gallois-Wong. Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie. Thèse de doctorat, Université Paris-Saclay, 2021. [ bib | full text on HAL ] |
[40] |
Raphaël Rieu-Helft.
Development and verification of arbitrary-precision integer
arithmetic libraries.
Thèse de doctorat, Université Paris-Saclay, 2020.
[ bib |
full text on HAL ]
Keywords: Static analysis ; Arbitrary-precision integer arithmetic ; Deductive verification of programs ; Proof by reflection ; Why3 ; Vérification déductive de programmes ; Arithmétique entière en précision arbitraire ; Analyse statique ; Preuve par réflexion ; Why3 |
[39] | Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Habilitation à diriger des recherches, Université Paris Sud, April 2019. [ bib | full text on HAL ] |
[38] | Albin Coquereau. Amélioration de performances du solveur SMT Alt-Ergo grâce à l'intégration d'un solveur SAT efficace. Thèse de doctorat, Université Paris-Saclay, 2019. [ bib | full text on HAL ] |
[37] | Florian Faissole. Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante. Thèse de doctorat, Université Paris Saclay, 2019. [ bib | full text on HAL ] |
[36] | Mattias Roux. Extensions de l'algorithme d'atteignabilité arrière dans le cadre de la vérification de modèles modulo théories. Thèse de doctorat, Université Paris Saclay, 2019. [ bib | full text on HAL ] |
[35] | Mário Pereira. Tools and Techniques for the Verification of Modular Stateful Code. Thèse de doctorat, Université Paris-Saclay, December 2018. [ bib ] |
[34] |
David Declerck.
Verification via Model Checking of Parameterized Concurrent
Programs on Weak Memory Models.
Thèse de doctorat, Université Paris-Saclay, September 2018.
[ bib |
full text on HAL ]
Keywords: Weak memory ; Model checking ; Verification ; Mémoire faible |
[33] | Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de doctorat, Université Paris-Saclay, March 2018. [ bib | full text on HAL ] |
[32] | Léon Gondelman. A Pragmatic Type System for Deductive Software Verification. Thèse de doctorat, Université Paris-Saclay, 2016. [ bib | full text on HAL ] |
[31] | Catherine Lelay. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. Thèse de doctorat, Université Paris-Sud, June 2015. [ bib | full text on HAL ] |
[30] | Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Thèse d'habilitation, Université Paris-Sud, October 2014. [ bib | full text on HAL ] |
[29] | Alain Mebsout. Invariants inference for model checking of parameterized systems. Thèse de doctorat, Université Paris-Sud, September 2014. [ bib | full text on HAL ] |
[28] | Évelyne Contejean. Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté. Thèse d'habilitation, Université Paris-Sud, June 2014. https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf. [ bib | full text on HAL ] |
[27] | Claire Dross. Generic Decision Procedures for Axiomatic First-Order Theories. Thèse de doctorat, Université Paris-Sud, April 2014. [ bib | full text on HAL ] |
[26] | Asma Tafat. Preuves par raffinement de programmes avec pointeurs. Thèse de doctorat, Université Paris-Sud, September 2013. [ bib | full text on HAL ] |
[25] | Mohamed Iguernelala. Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures. Thèse de doctorat, Université Paris-Sud, June 2013. [ bib | full text on HAL ] |
[24] | Cédric Auger. Compilation Certifiée de SCADE/LUSTRE. Thèse de doctorat, Université Paris-Sud, February 2013. http://tel.archives-ouvertes.fr/tel-00818169/. [ bib | full text on HAL ] |
[23] | Paolo Herms. Certification of a Tool Chain for Deductive Program Verification. Thèse de doctorat, Université Paris-Sud, January 2013. http://tel.archives-ouvertes.fr/tel-00789543. [ bib | full text on HAL ] |
[22] | Sylvain Conchon. SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Thèse d'habilitation, Université Paris-Sud, December 2012. In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf. [ bib | .html ] |
[21] | Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université Paris-Sud, June 2012. [ bib | full text on HAL | .pdf ] |
[20] | François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | full text on HAL | .pdf ] |
[19] | Jean-Christophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université Paris-Sud, December 2011. [ bib | .pdf ] |
[18] | Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Thèse de doctorat, Université Paris-Sud, October 2011. http://proval.lri.fr/publications/bardou11phd.pdf. [ bib | full text on HAL | .pdf ] |
[17] | Stéphane Lescuyer. Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud, January 2011. [ bib | full text on HAL | .pdf ] |
[16] | Xavier Urbain. Preuve automatique : techniques, outils et certification. Thèse d'habilitation, Université Paris-Sud 11, November 2010. [ bib ] |
[15] | Florence Plateau. Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ] |
[14] | Johannes Kanig. Spécification et preuve de programmes d'ordre supérieur. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ] |
[13] | Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ] |
[12] | Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [ bib ] |
[11] | Thierry Hubert. Analyse Statique et preuve de Programmes Industriels Critiques. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ] |
[10] | Nicolas Rousset. Automatisation de la Spécification et de la Vérification d'applications Java Card. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ] |
[9] | Nicolas Oury. Égalités et filtrages avec types dépendants dans le Calcul des Constructions Inductives. Thèse de doctorat, Université Paris-Sud, September 2006. [ bib ] |
[8] | Julien Signoles. Extension de ML avec raffinement : syntaxe, sémantiques et système de types. Thèse de doctorat, Université Paris-Sud, July 2006. [ bib ] |
[7] | June Andronick. Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation. Thèse de doctorat, Université Paris-Sud, March 2006. [ bib ] |
[6] | Louis Mandel. Conception, Sémantique et Implantation de ReactiveML : un langage à la ML pour la programmation réactive. PhD thesis, Université Paris 6, 2006. [ bib | PDF | .pdf ] |
[5] | Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ] |
[4] | Pierre Corbineau. Démonstration Automatique en Théorie des Types. Thèse de doctorat, Université Paris-Sud, September 2005. [ bib ] |
[3] | Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat, Université Paris-Sud, July 2004. [ bib | .ps.gz ] |
[2] | Jacek Chrzaszcz. Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University, Poland and Université de Paris-Sud, January 2004. [ bib ] |
[1] | Mihai Rotaru. Sur une théorie unificatrice des modèles de concurrence. PhD thesis, Cluj University, Romania and Université de Paris-Sud, January 2004. [ bib ] |
Misc.
[87] | Jean-Christophe Filliâtre. Structures de données semi-persistantes. Lecture at Collège de France, 2023. [ bib | full text on HAL ] |
[86] | Sylvie Boldo, François Clément, and Louise Leclerc. A Coq formalization of the Bochner integral. working paper or preprint, 2022. [ bib | full text on HAL ] |
[85] | Josué Moreau. Compilation formellement vérifiée d'un langage pour le calcul formel. working paper or preprint, 2022. [ bib | full text on HAL ] |
[84] | 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 ] |
[83] | Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller. Emulating round-to-nearest-ties-to-zero ”augmented” floating-point operations using round-to-nearest-ties-to-even arithmetic. working paper or preprint, October 2019. [ bib | full text on HAL ] |
[82] | Florian Steinberg, Laurent Thery, and Holger Thies. Quantitative continuity and computable analysis in Coq. working paper or preprint, April 2019. [ bib | full text on HAL | .pdf ] |
[81] | Florian Steinberg and Holger Thies. Some formal proofs of isomorphy and discontinuity. Third Workshop on Mathematical Logic and its Applications, March 2019. [ bib | full text on HAL ] |
[80] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.9, 2019. http://coq.inria.fr. [ bib | http ] |
[79] | Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. working paper https://hal.inria.fr/hal-01936105, November 2018. [ bib | full text on HAL ] |
[78] |
Anastasia Volkova, Thibault Hilaire, and Christoph Lauter.
Arithmetic approaches for rigorous design of reliable fixed-point
LTI filters.
working paper or preprint, November 2018.
[ bib |
full text on HAL ]
Keywords: Eigendecomposition ; Gershgorin circles ; Reliable Computations ; Floating-Point Arithmetic ; Digital Filters ; Interval Arithmetic ; Multiple Precision ; Fixed-Point Arithmetic ; Table Maker's Dilemma |
[77] | Jean-Christophe Filliâtre. Parcours d'un informaticien. Séminaire Info Pour Tous, September 2018. Séminaire invité. [ bib | http ] |
[76] | Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire. A Coq formalization of digital filters. August 2018. [ bib | DOI | full text on HAL | .pdf ] |
[75] | Jean-Christophe Filliâtre. An introduction to deductive program verification. Mathematical Summer in Paris (summer school), July 2018. Cours invité. [ bib ] |
[74] | 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 ] |
[73] | Andrei Paskevich and Thomas Wies, editors. Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ] |
[72] | 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 ] |
[71] | Alessandro Abate and Sylvie Boldo, editors. 10th International Workshop on Numerical Software Verification. Springer, July 2017. [ bib | full text on HAL ] |
[70] | 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 ] |
[69] | Florian Faissole and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. PPS 2017 - Workshop on probabilistic programming semantics, January 2017. Poster. [ bib | full text on HAL ] |
[68] | Sylvie Boldo and Julien Signoles, editors. Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ] |
[67] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.6, 2016. http://coq.inria.fr. [ bib | http ] |
[66] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.org/download/manual-0.86.1.pdf. [ bib | .pdf ] |
[65] | Thierry Vieville, Sylvie Boldo, Florent Masseglia, and Pierre Bernhard. Structures : organisation, complexité, dynamique des mot-clés au sens inattendu, April 2015. Article de vulgarisation sur pixees.fr. [ bib | full text on HAL ] |
[64] | Jean-Christophe Filliâtre. Vérification déductive de programmes. Mathematic Park, Institut Henri Poincaré, March 2015. Séminaire invité. [ bib | http ] |
[63] | Jacques Charles Mbiada Ndjanda. FCLLVM: un compilateur intégré à l'environnement Frama-C. Master's thesis, Université Paris-Diderot, 2014. https://www.lri.fr/~jmbiadan/public/cea_intership_v1.pdf. [ bib ] |
[62] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.org/download/manual-0.82.pdf. [ bib | .pdf ] |
[61] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform, version 0.81.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition,
March 2013.
http://why3.org/download/manual-0.81.pdf.
[ bib |
full text on HAL |
.pdf ]
Keywords: Why3 |
[60] |
Jean-Christophe Filliâtre.
Deductive program verification with Why3.
Lecture notes for the First DigiCosme Spring School,
https://usr.lmf.cnrs.fr/~jcf/digicosme-spring-school-2013/, 2013.
[ bib ]
Keywords: Why3 |
[59] | Martin Clochard. Proving programs with binders, automatically. Master's thesis, Master Parisien de Recherche en Informatique, 2013. [ bib ] |
[58] |
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Submitted, 2013.
[ bib |
full text on HAL |
.pdf ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists.
|
[57] | Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings., volume 7998 of Lecture Notes in Computer Science. Springer, 2013. [ bib | DOI | http ] |
[56] |
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 |
[55] |
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 |
[54] |
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 |
[53] | Nicolas Lupinski, Joel Falcou, and Christine Paulin-Mohring. Sémantiques d'un langage de squelettes. http://www.lri.fr/~paulin/Skel, 2012. [ bib ] |
[52] |
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 |
[51] | Nuno Gaspar. Mechanized semantics into concurrent program verification. http://www.lri.fr/~gaspar/rgcoq.html, September 2011. A documented Coq library, work in progress. [ bib ] |
[50] |
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition,
February 2011.
http://why3.org/.
[ bib ]
Keywords: Why3 |
[49] | Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in Frama-C --- Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib | PDF | http ] |
[48] | Philippe Audebaud and Christine Paulin-Mohring, editors. Science of Computer Programming. Special issue on the Mathematics of Program Construction (MPC 2008), volume 76. Elsevier Science Publishers, 2011. [ bib | DOI | http ] |
[47] | François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language, 2011. Preliminary report. http://hal.inria.fr/inria-00591414/. [ bib ] |
[46] | Catherine Lelay. étude de la différentiabilité et de l'intégrabilité en Coq : Application à la formule de d'Alembert pour l'équation des ondes. Master's thesis, Université Paris 7, 2011. http://www.lri.fr/~lelay/Rapport.pdf. [ bib ] |
[45] | Bernhard Beckert and Claude Marché, editors. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science. Springer, January 2011. [ bib ] |
[44] | Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, July 2010. http://interstices.info/decoupe. [ bib | http ] |
[43] | Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 5-12, http://www.universcience.tv/media/1340/l-informatique.html. [ bib | full text on HAL ] |
[42] | Sylvie Boldo. C'est la faute à l'ordinateur! Interstices -- Idée reçue, February 2010. http://interstices.info/idee-recue-informatique-18. [ bib | full text on HAL ] |
[41] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.3, 2010. http://coq.inria.fr. [ bib | http ] |
[40] | Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ] |
[39] | Sylvie Boldo. Demandez le programme! Interstices, February 2009. http://interstices.info/demandez-le-programme. [ bib | http ] |
[38] | Mohamed Iguernelala. Extension modulo Associativité-Commutativité de l'algorithme de clôture par congruence CC(X). Master's thesis, Université Paris-Sud, 2009. [ bib ] |
[37] | 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 ] |
[36] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
[35] | Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf. [ bib | .pdf ] |
[34] | Asma Tafat. Invariants et raffinements en présence de partage. Master's thesis, Université Paris 6, 2009. [ bib | .pdf ] |
[33] | Arthur Milchior. Algorithme de matching, modulo égalité, incrémental, typé et persistant. Rapport de stage L3, 2009. [ bib ] |
[32] | Claude Marché. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification, Viinistu, Estonia, January 2009. http://krakatoa.lri.fr/ws/. [ bib | PDF | http ] |
[31] | Paolo Herms. Partial type inference with higher-order types. Master's thesis, Università di Pisa, 2009. [ bib ] |
[30] | Sylvie Boldo and Thierry Viéville. L'informatique, ce n'est pas pour les filles. Interstices, September 2008. http://interstices.info/idee-recue-informatique-5. [ bib | http ] |
[29] | Philippe Audebaud and Christine Paulin-Mohring, editors. Mathematics of Program Construction, MPC 2008, volume 5133 of Lecture Notes in Computer Science, Marseille, France, July 2008. Springer. [ bib | http ] |
[28] | Sylvie Boldo. Pourquoi mon ordinateur calcule-t-il faux? Interstices, April 2008. Podcast, http://interstices.info/a-propos-calcul-ordinateurs. [ bib | http ] |
[27] | Maxime Beauquier. Application du filtrage modulo associativité et commutativité (AC) à la réécriture de sous-termes modulo AC dans Coq. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ] |
[26] | François Bobot. Satisfiabilité de formules closes modulo une théorie avec égalité et prédicats. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ] |
[25] | Steven Gay. Analyse d'échappement de portée en ReactiveML. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ] |
[24] | François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ] |
[23] | Sylvain Conchon and Évelyne Contejean. The Alt-Ergo automatic theorem prover. http://alt-ergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000. [ bib | http ] |
[22] | 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 ] |
[21] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.2, 2008. http://coq.inria.fr. [ bib | http ] |
[20] | Matthieu Sozeau. User defined equalities and relations, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ] |
[19] | Matthieu Sozeau. Program, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2, http://coq.inria.fr/. [ bib | http ] |
[18] | Matthieu Sozeau. Type Classes. INRIA, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ] |
[17] | Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ] |
[16] | Johannes Kanig. Certifying a congruence closure algorithm in Coq using traces. Diplomarbeit, Technische Universität Dresden, April 2007. [ bib ] |
[15] | Romain Bardou. Invariants de classe et systèmes d'ownership. Master's thesis, Master Parisien de Recherche en Informatique, 2007. [ bib | PDF | .pdf ] |
[14] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. CiME3, 2007. http://cime.lri.fr. [ bib | www: ] |
[13] | Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification, 2007. http://why.lri.fr/queens/. [ bib | PDF | http ] |
[12] | Louis Mandel and Luc Maranget. The JoCaml system, 2007. Software and documentation available at http://jocaml.inria.fr/. [ bib | http ] |
[11] | Alexandre Bertails. Langages synchrones avec horloges périodiques. Master's thesis, Master Parisien de Recherche en Informatique, September 2006. [ bib | PDF | .pdf ] |
[10] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.1, July 2006. http://coq.inria.fr. [ bib | http ] |
[9] | Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI, April 2006. [ bib | http ] |
[8] | Stéphane Lescuyer. Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master's thesis, Master Parisien de Recherche en Informatique, 2006. [ bib ] |
[7] | Nicolas Ayache. Coopération d'outils de preuve interactifs et automatiques. Master's thesis, Université Paris 7, 2005. [ bib ] |
[6] | Évelyne Contejean. Coccinelle, 2005. http://www.lri.fr/~contejea/Coccinelle/coccinelle.html. [ bib | www: ] |
[5] | Matthieu Sozeau. Coercion par prédicats en Coq. Master's thesis, Université Paris 7, 2005. In French. [ bib | .pdf ] |
[4] | Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers, volume 3839 of Lecture Notes in Computer Science. Springer, 2005. [ bib ] |
[3] | Thierry Hubert. Certification des preuves de terminaison en Coq. Rapport de DEA, Université Paris 7, September 2004. http://www.lri.fr/~marche/hubert04rr.ps. [ bib | .ps ] |
[2] | The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.0, April 2004. http://coq.inria.fr. [ bib | http ] |
[1] | G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 8.0, April 2004. [ bib | http ] |
Reports
[55] | Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and Raphaël Rieu-Helft. Formally verified bounds on rounding errors in concrete implementations of logarithm-sum-exponential functions. Research Report 9531, Inria, 2023. [ bib | full text on HAL ] |
[54] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. Lebesgue induction and Tonelli's theorem in Coq. Research Report 9457, Inria, 2023. [ bib | full text on HAL ] |
[53] | Jean-Christophe Filliâtre. Compte-rendu de fin de projet anr-15-ce25-0008 “vocal”. Technical report, Laboratoire Méthodes Formelles, June 2021. [ bib | full text on HAL ] |
[52] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Formal analysis of Ladder programs using deductive verification. Research Report RR-9402, Inria, April 2021. [ bib | full text on HAL ] |
[51] | Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Giant-step semantics for the categorisation of counterexamples. Research Report RR-9407, Inria, April 2021. [ bib | full text on HAL ] |
[50] |
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and
Micaela Mayero.
A Coq formalization of Lebesgue integration of nonnegative
functions.
Research Report RR-9401, Inria, France, 2021.
[ bib |
full text on HAL ]
Keywords: Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Théorie de la mesure ; Intégrale de Lebesgue |
[49] | Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. The Creusot environment for the deductive verification of Rust programs. Research Report 9448, Inria Saclay - Île de France, 2021. [ bib | full text on HAL ] |
[48] | Xavier Denis. Deductive program verification for a language with a Rust-like typing discipline. Internship report, Université de Paris, September 2020. [ bib | full text on HAL ] |
[47] | 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 ] |
[46] | Nicolas Jeannerod, Yann Régis-Gianas, Claude Marché, Mihaela Sighireanu, and Ralf Treinen. Specification of UNIX utilities. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ] |
[45] | Benedikt Becker, Claude Marché, Nicolas Jeannerod, and Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ] |
[44] | Léo Andrès. Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification. Rapport de stage de M1, Université Paris Sud, August 2019. [ bib | full text on HAL ] |
[43] | Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and Gidon Ernst. Verifythis 2018: A program verification competition. Research report, Université Paris-Saclay, January 2019. [ bib | full text on HAL ] |
[42] | Martin Clochard, Andrei Paskevich, and Claude Marché. Deductive verification via ghost debugging. Research Report 9219, Inria, 2018. [ bib | full text on HAL ] |
[41] | Lucas Baudin. Deductive verification with the help of abstract interpretation. Technical report, Univ Paris-Sud, November 2017. [ bib | full text on HAL ] |
[40] | Ilham Dami and Claude Marché. The CoLiS language: syntax, semantics and associated tools. Technical Report 0491, Inria, October 2017. [ bib | full text on HAL ] |
[39] | Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ] |
[38] | Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016. [ bib | full text on HAL ] |
[37] | David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria Saclay Ile-de-France, February 2016. [ bib | full text on HAL ] |
[36] |
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.
|
[35] | Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib | full text on HAL ] |
[34] | Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Fast parallel graph-search with splittable and catenable frontiers. Technical report, Inria, January 2015. [ bib | full text on HAL ] |
[33] | Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. Research Report 1560, LRI, June 2013. [ bib | full text on HAL | http | .pdf ] |
[32] |
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian,
Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane
Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia,
Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak,
Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane,
Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic,
Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin
Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi,
Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal
Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie
Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique
Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle
Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas,
Sophie De Quatrebarbes, and Stéphane Laurent.
Médiation scientifique : une facette de nos métiers de la
recherche.
Interne, Inria, March 2013.
[ bib |
full text on HAL |
http ]
Dans ce monde devenu numérique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du numérique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen maîtrise, au delà des usages, les principaux fondements de cette mutation numérique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque collègue Inria intéressé à participer à ce volet de nos missions. Devenue une facette de notre métier, comme le rappelle le Plan Stratégique Inria [1], ce que nous appelons médiation scientifique en sciences du numérique (alias, " mecsci ") se professionnalise et change d'échelle. Et c'est environ 1 % de nos ressources qui a vocation à y être consacré. Pour tout l'institut on parle donc de près de 40 équivalents temps-plein distribués à travers le travail quotidien ou ponctuel de plusieurs centaines de collègues chercheurs, ingénieurs, communicants, etc.. Une telle énergie mérite d'être bien employée : au service des meilleurs objectifs ; vers des cibles bien définies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident à faire bouger les choses ; et avec une méthodologie efficace qui optimise ce que nous investissons dans de telles activités ; tout en respectant et en encourageant les dynamiques locales et individuelles indépendantes qui restent les sources vives de la médiation scientifique. Voilà pourquoi il y a juste besoin d'offrir en partage à chacune et chacun les éléments fondateurs et méthodologiques de cette médiation scientifique. Offrir aussi quelques bonnes pratiques très concrètes. On parle donc ici d'une organisation distribuée d'actions collaboratives d'où émerge le service public de popularisation scientifique visé. C'est ce que ce document se propose de décrire ici. Keywords: médiation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public. |
[31] | Claude Marché and Asma Tafat. Weakest precondition calculus, revisited using Why3. Research Report RR-8185, INRIA, December 2012. [ bib | full text on HAL | .pdf ] |
[30] |
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR-7986, INRIA, June 2012.
[ bib |
full text on HAL |
.pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism. Keywords: Quantifiers, Triggers, SMT Solvers, Theories |
[29] | Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Technical report, Tech. Univ. Munich, 2012. http://www21.in.tum.de/~blanchet/tff1spec.pdf. [ bib | .pdf ] |
[28] |
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 |
[27] |
Asma Tafat and Claude Marché.
Binary heaps formally verified in Why3.
Research Report 7780, INRIA, October 2011.
http://hal.inria.fr/inria-00636083/en/.
[ bib |
full text on HAL ]
Keywords: Why3 |
[26] | Krishnamani Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. http://hal.inria.fr/inria-00615623/en/. [ bib | full text on HAL ] |
[25] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib | .pdf | Abstract ] |
[24] | Thi Minh Tuyen Nguyen and Claude Marché. Proving floating-point numerical programs by analysis of their assembly code. Research Report 7655, INRIA, 2011. http://hal.inria.fr/inria-00602266/en/. [ bib | full text on HAL ] |
[23] | Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. Research Report 7793, INRIA, 2011. http://hal.inria.fr/hal-00639977/en/. [ bib | full text on HAL ] |
[22] | Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib | PDF | .pdf | Abstract ] |
[21] | Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform (version 2). Technical Report 7128, INRIA, 2010. http://hal.inria.fr/inria-00439232/en/. [ bib | full text on HAL ] |
[20] | Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement approach for correct-by-construction object-oriented programs. Technical Report 7310, INRIA, 2010. [ bib | full text on HAL ] |
[19] | Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Research Report 7412, INRIA, 2010. http://hal.inria.fr/inria-00525384/en/. [ bib | full text on HAL ] |
[18] | Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. Technical Report 7128, INRIA, 2009. http://hal.inria.fr/inria-00439232. [ bib | full text on HAL ] |
[17] |
Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko.
Modular specification of Java programs.
Technical Report 7097, INRIA, 2009.
[ bib |
full text on HAL ]
This work investigates the question of modular specification of generic Java classes and methods. The first part introduces a specification language for Java programs. In the second part the language is used to specify an array sorting algorithm by selection. The third and the fourth parts define a syntax proposal for the specification a generic Java programs, through two examples. The former is the specification of the generic method for sorting arrays which comes in the java.util.Arrays class of the Java API. The latter is the specification of the java.util.HashMap class and its use for memoization.
|
[16] | Ali Ayad. On formal methods for certifying floating-point C programs. Research Report 6927, INRIA, 2009. [ bib | full text on HAL ] |
[15] | Guillaume Melquiond and Sylvain Pion. Directed rounding arithmetic operations. Technical Report 2899, ISO C++ Standardization Committee, 2009. [ bib ] |
[14] | Jean-François Couchot, Alain Giorgetti, and Nicolas Stouls. Graph-based Reduction of Program Verification Conditions. Research Report 6702, INRIA Saclay -- Île-de-France, October 2008. [ bib | full text on HAL ] |
[13] | Évelyne Contejean, Julien Forest, and Xavier Urbain. Deep-Embedded Unification. Research Report 1547, Cédric laboratory, CNAM Paris, France, 2008. [ bib ] |
[12] | Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq - version 2. Description of a Coq contribution, Université Paris Sud, December 2007. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ] |
[11] | Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ] |
[10] | Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Research Report 1185, CEDRIC, May 2007. [ bib ] |
[9] | Louis Mandel and Luc Maranget. Programming in JoCaml -- extended version. Technical Report 6261, INRIA, 2007. [ bib | PDF | .pdf ] |
[8] | Louis Mandel. Prototype of AADL simulation in SCADE. ASSERT deliverable 4.3.2-2, ASSERT Project, November 2006. [ bib ] |
[7] | Julien Signoles. Towards a ML extension with Refinement: a Semantic Issue. Technical Report 1440, LRI, University of Paris Sud, March 2006. [ bib | .pdf ] |
[6] | Louis Mandel. Report on modeling GALS in SCADE. ASSERT deliverable 4.3.2-1, ASSERT Project, February 2006. [ bib ] |
[5] | Jean-Christophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib | .ps.gz ] |
[4] | Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq. Description of a Coq contribution, Université Paris Sud, January 2006. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ] |
[3] | Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Research Report DSIC II/01/05, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2005. [ bib ] |
[2] | Vikrant Chaudhary. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A case study. Technical report, IIT internship report, July 2004. [ bib ] |
[1] | Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ] |
Back
Books / Journals / Conferences / PhD theses / Misc. / Reports
This page was generated by bibtex2html.