[1] |
Jean-Christophe Filliâtre and Claude Marché.
Multi-Prover Verification of C Programs.
In Sixth International Conference on Formal Engineering Methods
(ICFEM), Seattle, November 2004.
To appear.[ bib | .ps.gz ]
Our goal is the verification of C programs at the source code level using formal proof tools. Programs are specified using annotations such as pre- and postconditions and global invariants. An original approach is presented which allows to formally prove that a function implementation satisfies its specification and is free of null pointer dereferencing and out-of-bounds array access. The method is not bound to a particular back-end theorem prover. A significant part of the ANSI C language is supported, including pointer arithmetic and possible pointer aliasing. We describe a prototype tool and give some experimental results. |

[2] |
J.-C. Filliâtre and P. 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 | .ps.gz ]
This paper presents the formal verification with the Coq proof assistant of several applicative data structures implementing finite sets. These implementations are parameterized by an ordered type for the elements, using functors from the ML module system. The verification follows closely this scheme, using the newly Coq module system. One of the verified implementation is the actual code for sets and maps from the Objective Caml standard library. The formalization refines the informal specifications of these libraries into formal ones. The process of verification exhibited two small errors in the balancing scheme, which have been fixed and then verified. Beyond these verification results, this article illustrates the use and benefits of modules and functors in a logical framework. |

[3] |
J.-C. Filliâtre.
Why: a multi-language multi-prover verification tool.
Research Report 1366, LRI, Université Paris Sud, March 2003. [ bib | .ps.gz ] |

[4] |
J.-C. Filliâtre and F. Pottier.
Producing All Ideals of a Forest, Functionally.
Journal of Functional Programming, 13(5):945-956, September
2003.[ bib | .ps.gz ]
We present a functional implementation of Koda and Ruskey's algorithm for generating all ideals of a forest poset as a Gray code. Using a continuation-based approach, we give an extremely concise formulation of the algorithm's core. Then, in a number of steps, we derive a first-order version whose efficiency is comparable to a C implementation given by Knuth. |

[5] |
J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar.
Deciding propositional combinations of equalities and inequalities.
Unpublished, October 2001. [ bib | .ps ]
We address the problem of combining individual decision procedures into a single decision procedure. Our combination approach is based on using the canonizer obtained from Shostak's combination algorithm for equality. We illustrate our approach with a combination algorithm for equality, disequality, arithmetic inequality, and propositional logic. Unlike the Nelson-Oppen combination where the processing of equalities is distributed across different closed decision procedures, our combination involves the centralized processing of equalities in a single procedure. The termination argument for the combination is based on that for Shostak's algorithm. We also give soundness and completeness arguments. |

[6] |
J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar.
ICS: Integrated Canonization and Solving (Tool presentation).
In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of
CAV'2001, volume 2102 of Lecture Notes in Computer Science, pages
246-249. Springer-Verlag, 2001.[ bib ] |

[7] |
J.-C. Filliâtre.
La supériorité de l'ordre supérieur.
In Journées Francophones des Langages Applicatifs, pages
15-26, Anglet, France, Janvier 2002.[ bib | .ps.gz ]
Nous présentons ici une écriture fonctionnelle de l'algorithme de Koda-Ruskey, un algorithme pour engendrer une large famille de codes de Gray. En s'inspirant de techniques de programmation par continuation, nous aboutissons à un code de neuf lignes seulement, bien plus élégant que les implantations purement impératives proposées jusqu'ici, notamment par Knuth. Dans un second temps, nous montrons comment notre code peut être légèrement modifié pour aboutir à une version de complexité optimale. Notre implantation en Objective Caml rivalise d'efficacité avec les meilleurs codes C. Nous détaillons les calculs de complexité, un exercice intéressant en présence d'ordre supérieur et d'effets de bord combinés. |

[8] |
J.-C. Filliâtre.
Design of a proof assistant: Coq version 7.
Research Report 1369, LRI, Université Paris Sud, October 2000. [ bib | .ps.gz ]
We present the design and implementation of the new version of the Coq proof assistant. The main novelty is the isolation of the critical part of the system, which consists in a type checker for the Calculus of Inductive Constructions. This kernel is now completely independent of the rest of the system and has been rewritten in a purely functional way. This leads to greater clarity and safety, without compromising efficiency. It also opens the way to the ``bootstrap'' of the Coq system, where the kernel will be certified using Coq itself. |

[9] |
J.-C. Filliâtre.
Hash consing in an ML framework.
Research Report 1368, LRI, Université Paris Sud, September
2000. [ bib | .ps.gz ]
Hash consing is a technique to share values that are structurally equal. Beyond the obvious advantage of saving memory blocks, hash consing may also be used to gain speed in several operations (like equality test) and data structures (like sets or maps) when sharing is maximal. However, physical adresses cannot be used directly for this purpose when the garbage collector is likely to move blocks underneath. We present an easy solution in such a framework, with many practical benefits. |

[10] |
J.-C. Filliâtre and C. Marché.
ocamlweb, a literate programming tool for Objective Caml.
Available at http://www.lri.fr/~filliatr/ocamlweb/. [ bib | http ] |

[11] |
J.-C. Filliâtre.
Verification of Non-Functional Programs using Interpretations in
Type Theory.
Journal of Functional Programming, 13(4):709-745, July 2003.
English translation of [14].[ bib | .ps.gz ]
We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory constitutes a powerful specification language, which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program, and on the use of monads. The usual notion of monads is refined in order to account for the notion of effect. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. We also establish a result of partial completeness. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic. |

[12] |
J.-C. Filliâtre.
Formal Proof of a Program: Find.
Science of Computer Programming, 2001.
To appear.[ bib | .ps.gz ]
In 1971, C. A. R. Hoare gave the proof of correctness and termination of a rather complex algorithm, in a paper entitled |

[13] |
J.-C. Filliâtre.
A theory of monads parameterized by effects.
Research Report 1367, LRI, Université Paris Sud, November 1999. [ bib | .ps.gz ]
Monads were introduced in computer science to express the semantics of programs with computational effects, while type and effect inference was introduced to mark out those effects. In this article, we propose a combination of the notions of effects and monads, where the monadic operators are parameterized by effects. We establish some relationships between those generalized monads and the classical ones. Then we use a generalized monad to translate imperative programs into purely functional ones. We establish the correctness of that translation. This work has been put into practice in the Coq proof assistant to establish the correctness of imperative programs. |

[14] |
J.-C. Filliâtre.
Preuve de programmes impératifs en théorie des types.
Thèse de doctorat, Université Paris-Sud, July 1999.[ bib | .ps.gz ]
Nous étudions le problème de la certification de programmes mêlant traits impératifs et fonctionnels dans le cadre de la théorie des types. |

[15] |
J.-C. Filliâtre and N. Magaud.
Certification of sorting algorithms in the system Coq.
In Theorem Proving in Higher Order Logics: Emerging Trends,
1999.[ bib | .ps.gz ]
We present the formal proofs of total correctness of three sorting algorithms in the system Coq, namely |

[16] |
J.-C. Filliâtre.
Proof of Imperative Programs in Type Theory.
In International Workshop, TYPES '98, Kloster Irsee, Germany,
volume 1657 of Lecture Notes in Computer Science. Springer-Verlag,
March 1998.[ bib | .ps.gz ]
We present a new approach to certifying imperative programs, in the context of Type Theory. The key is a functional translation of imperative programs, which is made possible by an analysis of their effects. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic, but our approach also includes functional constructions. As a side-effect, we propose a way to eradicate the use of auxiliary variables in specifications. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples. |

[17] |
J.-C. Filliâtre.
Finite Automata Theory in Coq: A constructive proof of Kleene's
theorem.
Research Report 97-04, LIP - ENS Lyon, February 1997. [ bib | .ps.Z ]
We describe here a development in the system Coq of a piece of Finite Automata Theory. The main result is the Kleene's theorem, expressing that regular expressions and finite automata define the same languages. From a constructive proof of this result, we automatically obtain a functional program that compiles any regular expression into a finite automata, which constitutes the main part of the implementation of |

[18] |
J.-C. Filliâtre.
A decision procedure for Direct Predicate Calculus: study and
implementation in the Coq system.
Research Report 96-25, LIP - ENS Lyon, February 1995. [ bib | .ps.Z ]
The paper of J. Ketonen and R. Weyhrauch |

[19] |
J.-C. Filliâtre.
Une procédure de décision pour le Calcul des Prédicats
Direct : étude et implémentation dans le système Coq.
Rapport de DEA, Ecole Normale Supérieure, Juillet 1994. [ bib | .dvi.gz ] |

[20] |
J. Courant et J.-C. Filliâtre.
Formalisation de la théorie des langages formels en Coq.
Rapport de maîtrise, Ecole Normale Supérieure, Septembre 1993. [ bib | .dvi.gz ] |

*This file has been generated by
bibtex2html 1.73*