[25] 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 ]
[24] 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.

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

[22] É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 ]
[21] 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.

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

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

[18] 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 ]
[17] 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 ]
[16] 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 ]
[15] 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.

[14] 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 ]
[13] 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 ]
[12] 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.

[11] 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 ]
[10] 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 ]
[9] 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 ]
[8] 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 ]
[7] 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.

[6] 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 ]
[5] 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.

[4] 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 ]
[3] 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 ]
[2] 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.

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