Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications since 2004

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

[12] Jean-Christophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib | http ]
[11] Christine Paulin-Mohring. Course notes LASER summerschool 2011, chapter Introduction to the Coq proof-assistant for practical software verification. Lecture Notes in Computer Science. Springer, 2012. to appear. [ bib | .pdf ]
[10] 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 ]
[9] 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 ]
[8] 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 ]
[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 paper 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

[29] V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyen. Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems (TODS), 2013. To appear. [ bib ]
[28] 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, 2012. [ bib | full paper on HAL ]
[27] Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14-23, 2012. [ bib | DOI ]
[26] 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, 2012. Accepted for publication. http://hal.inria.fr/hal-00649240/en/. [ bib | full paper on HAL ]
[25] 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, 2012. Accepted for publication. [ bib ]
[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 paper 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 paper 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 ]
[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 | .pdf ]
[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), 2010. [ bib | DOI | full paper 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 paper 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 | full paper on HAL | PDF ]
[15] Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220-225, February 2009. [ bib | DOI | full paper on HAL | PDF ]
[14] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568-589, 2009. [ bib | DOI | full paper on HAL | PDF ]
[13] 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 ]
[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 | 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 | full paper on HAL | PDF ]
[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

[154] 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 ]
[153] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. In Proceedings of the The Second International Conference on Certified Programs and Proofs, Kyoto, Japan, December 2012. [ bib | full paper on HAL ]
[152] 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 | .pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.

[151] 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 ]
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.

[150] David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine Paulin-Mohring. Towards Provably Robust Watermarking. In ITP 2012, August 2012. [ bib | .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
[149] 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, Lecture Notes in Computer Science, Berkeley, California, USA, July 2012. Springer. [ bib ]
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.

[148] 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.

In this article, we present a new algorithm which solves the subtyping constraints generated by the clock calculus. The advantage of this algorithm is that it finds schedules for tightly coupled systems. Moreover, it does not overestimate the buffer sizes needed and it provides a way to favor either system throughput or buffer size minimization.

[147] 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, Lecture Notes in Computer Science, Pisa, Italy, June 2012. Springer. http://hal.inria.fr/hal-00681781/en/. [ bib | full paper 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.

[146] François Bobot, Sylvain Conchon, Evelyne 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 ]
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.

[145] 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 | .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.

[144] 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 ]
[143] 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 paper on HAL ]
[142] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, VSTTE, Lecture Notes in Computer Science. Springer, 2012. [ bib | .pdf ]
[141] Jean-Christophe Filliâtre. Verifying two lines of C with Why3: an exercise in program verification. In Verified Software: Theories, Tools and Experiments (VSTTE), Philadelphia, USA, January 2012. [ 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.

[140] 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, Lecture Notes in Computer Science. Springer, 2012. [ bib | .pdf ]
[139] 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, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ]
[138] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ]
[137] 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 ]
[136] 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 (LIPIcs), pages 133-148, Nagoya, Japan, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [ bib ]
[135] 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. Springer, December 2011. [ bib ]
[134] 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 | .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.

[133] 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 ]
[132] 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. [ bib | .pdf ]
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.

[131] 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 | .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.

[130] Jean-Christophe Filliâtre and K. 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 ]
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.

[129] 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 | .pdf | Abstract ]
[128] 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.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the SUNDIALS library.

[127] 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 ]
[126] É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 (LIPIcs), pages 21-30, Novi Sad, Serbia, 2011. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [ bib | DOI | http | Abstract ]
[125] 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 ]
[124] 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 ]
[123] 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 ]
[122] 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.

[121] 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 | .pdf ]
[120] 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 ]
[119] 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 ]
[118] 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 ]
[117] 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 ]
[116] M. Barbosa, Jean-Christophe Filliâtre, J. Sousa Pinto, and B. 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 ]
[115] 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 | .pdf ]
[114] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147-162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2). [ bib | full paper on HAL ]
[113] 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 paper on HAL ]
[112] 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 ]
[111] 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.

This paper presents the first implementation of the n-synchronous model inside a Lustre-like language called Lucy-n. The language extends Lustre with an explicit buffer construct whose size is automatically computed during the clock calculus. This clock calculus is defined as an inference type system and is parametrized by the clock language and the algorithm used to solve subtyping constraints. We detail here one algorithm based on the abstraction of clocks, an idea originally introduced in [83]. The paper presents a simpler, yet more precise, clock abstraction for which the main algebraic properties have been proved in Coq. Finally, we illustrate the language on various examples including a video application.

[110] 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 paper on HAL | PDF ]
[109] Louis Mandel, Florence Plateau, and Marc Pouzet. Clock typing of n-synchronous programs. In Designing Correct Circuits (DCC 2010), Paphos, Cyprus, March 2010. [ bib ]
[108] 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 ]
[107] 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 ]
[106] É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 ]
[105] 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 ]
[104] É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 ]
[103] 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 ]
[102] 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.

Nous avons présenté l'année dernière un article décrivant comment abstraire des horloges pour vérifier la relation de sous-typage. Cette année, nous présentons un langage de programmation n-synchrone : Lucy-n. Dans ce langage, l'inférence des types d'horloges est paramétrable par l'algorithme de résolution des contraintes de sous-typage. Nous montrons ici un algorithme basé sur les travaux de l'an dernier et comment programmer en Lucy-n à travers l'exemple d'une application de traitement multimédia.

[101] 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 ]
[100] 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 paper on HAL ]
[99] Paolo Herms. Certification of a chain for deductive program verification. In Yves Bertot, editor, 2nd Coq Workshop, satellite of ITP'10, 2010. [ 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] 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 ]
[96] 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 ]
[95] 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 | .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.

[94] Louis Mandel, Florence Plateau, and Marc Pouzet. The ReactiveML toplevel (tool demonstration). In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [ bib ]
[93] 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 ]
[92] Sylvie Boldo. Floats & 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 - ARCoSS, pages 91-102, Rhodos, Greece, July 2009. Springer. [ bib ]
[91] 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 | .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).

[90] 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 ]
[89] 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 ]
[88] 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 ]
[87] 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 ]
[86] 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.

[85] 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 [83] 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.

[84] 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 ]
[83] 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), 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.

[82] 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. [ 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.

[81] 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.

[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 paper 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] 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 ]
[74] Évelyne Contejean. Coccinelle, a Coq library for rewriting. In Types, Torino, Italy, March 2008. [ bib ]
[73] 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 ]
[72] 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 ]
[71] 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.

[70] 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.

[69] Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]
[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. [ 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. http://knuth07.labri.fr/exposes.php. [ bib | PDF | .pdf ]
We introduce a methodology to formally verify MIX programs. It consists in annotating a MIX program with logical annotations and then to turn it into a set of purely sequential programs on which classical techniques can be applied. Contrary to other approaches of verification of unstructured programs, we do not impose the location of annotations but only the existence of at least one invariant on each cycle in the control flow graph. A prototype has been implemented and used to verify several programs from The Art of Computer Programming.

[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 | PDF | .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] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, pages 187-194, Montpellier, France, June 2007. [ bib | PDF | .pdf ]
This paper introduces a methodology to perform formal verification of floating-point C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floating-point arithmetic. The Caduceus first-order logic model for C programs is extended accordingly. Then verification conditions expressing the correctness of the programs are obtained in the usual way and can be discharged interactively with the Coq proof assistant, using an existing Coq formalization of floating-point arithmetic. This methodology is already implemented and has been successfully applied to several short floating-point programs, which are presented in this paper.

[51] 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 ]
[50] 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 ]
[49] 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.

[48] 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 ]
[47] 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 | PDF | .pdf ]
[46] 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 ]
[45] 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 ]
[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.

Cependant, le caractère impératif de cette structure de données devient gênant lorsqu'elle est utilisée dans un contexte où s'effectuent des retours en arrière (backtracking). Nous présentons dans cet article une version persistante de union-find dont la complexité est comparable à celle de la solution impérative. Pour obtenir cette efficacité, notre solution utilise massivement des traits impératifs. C'est pourquoi nous présentons également une preuve formelle de correction, pour s'assurer notamment du caractère persistant de cette solution.

[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. [ bib | DOI | http ]
[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 | .ps ]
[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. [ 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 paper 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 | PDF | .pdf ]
[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 | PDF | .pdf ]
[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

[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 | .pdf ]
[20] François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | .pdf ]
[19] Jean-Christophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université Paris-Sud, December 2011. http://www.lri.fr/~filliatr/hdr/memoire.pdf. [ 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 | .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 | .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 | PDF | .pdf ]
[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.

[53] 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. https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf. [ bib ]
[52] 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. https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf. [ bib ]
[51] 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 ]
[50] 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 ]
[49] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.lri.fr/. [ bib ]
[48] 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 ]
[47] 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 ]
[46] François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language, 2011. Preliminary report. http://hal.inria.fr/inria-00591414/. [ bib ]
[45] 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 ]
[44] 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 ]
[43] Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, July 2010. http://interstices.info/decoupe. [ bib | http ]
[42] Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 5-12, http://www.universcience.tv/media/1340/l-informatique.html. [ bib | full paper on HAL ]
[41] Sylvie Boldo. C'est la faute à l'ordinateur! Interstices - Idée reçue, February 2010. http://interstices.info/idee-recue-informatique-18. [ bib | full paper on HAL ]
[40] The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.3, 2010. http://coq.inria.fr. [ bib | http ]
[39] Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ]
[38] Sylvie Boldo. Demandez le programme! Interstices, February 2009. http://interstices.info/demandez-le-programme. [ bib | http ]
[37] Mohamed Iguernelala. Extension modulo Associativité-Commutativité de l'algorithme de clôture par congruence CC(X). Master's thesis, Université Paris-Sud, 2009. [ bib ]
[36] 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 ]
[35] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[34] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf. [ bib | .pdf ]
[33] Asma Tafat. Invariants et raffinements en présence de partage. Master's thesis, Université Paris 6, 2009. [ bib | .pdf ]
[32] Arthur Milchior. Algorithme de matching, modulo égalité, incrémental, typé et persistant. Rapport de stage L3, 2009. [ bib ]
[31] 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 ]
[30] Paolo Herms. Partial type inference with higher-order types. Master's thesis, Università di Pisa, 2009. [ bib ]
[29] 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 ]
[28] 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 ]
[27] Sylvie Boldo. Pourquoi mon ordinateur calcule-t-il faux? Interstices, April 2008. Podcast, http://interstices.info/a-propos-calcul-ordinateurs. [ bib | http ]
[26] 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 ]
[25] 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 ]
[24] Steven Gay. Analyse d'échappement de portée en ReactiveML. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ]
[23] 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 ]
[22] 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 ]
[21] 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 ]
[20] The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.2, 2008. http://coq.inria.fr. [ bib | http ]
[19] Matthieu Sozeau. User defined equalities and relations, 2008. Chapter of The Coq Proof Assistant Reference Manual - Version V8.2. [ bib ]
[18] Matthieu Sozeau. Program, 2008. Chapter of The Coq Proof Assistant Reference Manual - Version V8.2, http://coq.inria.fr/. [ bib | http ]
[17] Matthieu Sozeau. Type Classes. INRIA, 2008. Chapter of The Coq Proof Assistant Reference Manual - Version V8.2. [ bib ]
[16] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[15] Johannes Kanig. Certifying a congruence closure algorithm in Coq using traces. Diplomarbeit, Technische Universität Dresden, April 2007. [ bib ]
[14] Romain Bardou. Invariants de classe et systèmes d'ownership. Master's thesis, Master Parisien de Recherche en Informatique, 2007. [ bib | PDF | .pdf ]
[13] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. CiME3, 2007. http://cime.lri.fr. [ bib | www: ]
[12] Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification, 2007. http://why.lri.fr/queens/. [ bib | PDF | http ]
[11] Louis Mandel and Luc Maranget. The JoCaml system, 2007. Software and documentation available at http://jocaml.inria.fr/. [ bib | http ]
[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

[30] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. Research Report RR-7986, INRIA, June 2012. [ bib | full paper 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] 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. http://hal.inria.fr/hal-00649240/en/. [ bib | full paper on HAL | .pdf ]
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
[28] 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 paper on HAL ]
[27] K. 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 paper on HAL ]
[26] É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 ]
[25] 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 paper on HAL ]
[24] 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 paper on HAL ]
[23] Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. Technical report, INRIA, 2011. [ bib | full paper 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 paper 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 paper 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 paper 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/en/. [ bib | full paper on HAL ]
[17] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Modular specification of Java programs. Technical Report 7097, INRIA, 2009. [ bib | full paper 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 paper 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 paper 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.