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

[mlpost09jfla] Romain Bardou and Jean-Christophe Filliâtre and 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 [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.

[conchon08entcs] Sylvain Conchon and Evelyne Contejean and Johannes Kanig and Stéphane Lescuyer. CC(X): Semantic Combination of Congruence Closure with Solvable Theories. In Electr. Notes Theor. Comput. Sci.198(2):51-69 2008 [bib] [pdf]

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.

[conchon08jfla] Sylvain Conchon and 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 [bib] [pdf]

Le problème SAT, qui consiste à 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 ainsi qu'une mise en forme normale conjonctive paresseuse. 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.

[conchon07afm] Sylvain Conchon and Evelyne Contejean and Johannes Kanig and Stéphane Lescuyer. Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In AFM07 (Automated Formal Methods), Atlanta, Georgia, USA, November 2007 [bib] [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.

[conchonsmt07] Sylvain Conchon and Evelyne Contejean and Johannes Kanig. CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers. In 5th International Workshop on Satisfiability Modulo, Berlin, Germany, July 2007 [bib] [pdf]

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and a union X of solvable theories. 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 approach by the use of semantical values for class representatives instead of syntactical canonizers. This seemingly insignificant difference has strong impact on efficiency and expressiveness. 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.