[25]  Dariusz Biernacki, JeanLouis Colaço, and Marc Pouzet. Clockdirected 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 JeanChristophe Filliâtre.
A Persistent UnionFind Data Structure.
In ACM SIGPLAN Workshop on ML, pages 3745, Freiburg, Germany,
October 2007. ACM.
[ bib 
PDF 
.pdf ]
The problem of disjoint sets, also known as unionfind, 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 unionfind 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] 
JeanChristophe 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 148162, Liverpool,UK, September 2007. Springer. [ bib  DOI  Abstract ] 
[21] 
JeanFrançois Couchot and Thierry Hubert.
A Graphbased Strategy for the Selection of Hypotheses.
In FTP 2007  International Workshop on FirstOrder 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] 
JeanFrançois Couchot and Stéphane Lescuyer.
Handling polymorphism in automated deduction.
In 21th International Conference on Automated Deduction
(CADE21), volume 4603 of LNCS (LNAI), pages 263278, Bremen,
Germany, July 2007.
[ bib 
PDF 
.pdf ]
Polymorphism has become a common way of designing short and reusable programs by abstracting generic definitions from typespecific 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 SMTLIB ones do not handle polymorphism. To this end, we present efficient reductions of polymorphism in both unsorted and manysorted 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] 
JeanFranç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 176194, 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, counterexample 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 settheoretical constraint solver and some modelcheckers.

[18]  JeanChristophe 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 173177, 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 ICISR07015, pages 116. 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 8499, Paris, France, June 2007. [ bib  PDF  .pdf ] 
[15] 
Sylvie Boldo and JeanChristophe Filliâtre.
Formal Verification of FloatingPoint Programs.
In 18th IEEE International Symposium on Computer Arithmetic,
pages 187194, Montpellier, France, June 2007.
[ bib 
PDF 
.pdf ]
This paper introduces a methodology to perform formal verification of floatingpoint C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floatingpoint arithmetic. The Caduceus firstorder 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 floatingpoint arithmetic. This methodology is already implemented and has been successfully applied to several short floatingpoint 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 303313, 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/terminationcompetition/. [ bib  http ] 
[12] 
Sylvain Conchon, JeanChristophe 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 TRSHUCS2007041,
pages XII/113, 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 structuresdirected 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 socalled functors.

[11]  Sylvain Conchon, JeanChristophe 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 8193, 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 ComponentBased Software Architectures (FESCA'07), pages 123136. 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 3551, 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 5559. 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 builtin 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 JeanChristophe Filliâtre.
UnionFind Persistant.
In Dixhuitièmes Journées Francophones des Langages
Applicatifs, pages 135149. INRIA, January 2007.
[ bib 
PDF 
.pdf ]
Le problème des classes disjointes, connu sous le nom de unionfind, 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.

[4]  Sébastien Labbé, JeanPierre 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 12, 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 1821, 2006, Revised Selected Papers, volume 4502 of Lecture
Notes in Computer Science, pages 237252. 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 typechecking conditions). A prototype implementation of this process is integrated with the Coq environment.

[1] 
Matthieu Sozeau.
Programing finger trees in Coq.
In Ralf Hinze and Norman Ramsey, editors, 12th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2007, pages 1324,
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.
