@inproceedings{KanigFilliatre09wml,
author = {Johannes Kanig and Jean-Christophe Filli\^atre},
title = {{Who: A Verifier for Effectful Higher-order Programs}},
booktitle = {ACM SIGPLAN Workshop on ML},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
year = 2009,
month = aug,
address = {Edinburgh, Scotland, UK},
abstract = {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.},
url = {http://www.lri.fr/~kanig/publis/wml09.pdf}
}
@inproceedings{mlpost09jfla,
author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
title = {{Faire bonne figure avec Mlpost}},
booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
year = 2009,
month = jan,
address = {Saint-Quentin sur Is\`ere},
abstract = {Cet article pr\'esente Mlpost, une biblioth\`eque 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\'eduisante aux langages de macros \LaTeX, aux langages
sp\'ecialis\'es ou m\^eme aux outils graphiques. En particulier,
l'utilisateur de Mlpost b\'en\'eficie de toute l'expressivit\'e
d'Ocaml et de son typage statique. Enfin Mlpost propose un style
d\'eclaratif qui diff\`ere de celui, souvent imp\'eratif, des outils existants.},
url = {http://www.lri.fr/~kanig/publis/mlpost-fra.pdf},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
publisher = {INRIA}
}
@article{conchon08entcs,
author = {Sylvain Conchon and
Evelyne Contejean and
Johannes Kanig and
St{\'e}phane Lescuyer},
title = {CC(X): Semantic Combination of Congruence Closure with Solvable
Theories},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {198},
number = {2},
year = {2008},
pages = {51-69},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.04.080},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {
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.
},
url = {http://www.lri.fr/~kanig/publis/cckl-entcs08.pdf}
}
@inproceedings{conchon08jfla,
author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
title = {{SAT-Micro : petit mais costaud!}},
booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
year = 2008,
month = {JAN},
address = {\'Etretat, France},
publisher = {INRIA},
abstract = {
Le probl\`eme SAT, qui consiste \`a d\'eterminer si une formule bool\'eenne
est satisfaisable, est un des probl\`emes NP-complets les plus
c\'el\`ebres et aussi un des plus \'etudi\'es. Bas\'es initialement sur la
proc\'edure DPLL, les SAT-solvers modernes ont connu des
progr\`es spectaculaires ces dix derni\`eres ann\'ees dans leurs
performances, essentiellement gr\^ace \`a deux optimisations: le retour
en arri\`ere non-chronologique et l'apprentissage par analyse des
clauses conflits. Nous proposons dans cet article une \'etude formelle
du fonctionnement de ces techniques ainsi qu'une r\'ealisation en
Ocaml d'un SAT-solver, baptis\'e SAT-Micro, int\'egrant ces
optimisations ainsi qu'une mise en forme normale conjonctive
paresseuse. Le fonctionnement de SAT-Micro est d\'ecrit par un
ensemble de r\`egles d'inf\'erence et la taille de son code, 70 lignes
au total, permet d'envisager sa certification compl\`ete.
},
url = {http://www.lri.fr/~kanig/publis/ckl-jfla08.ps}
}
@inproceedings{conchon07afm,
author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig and St{\'e}phane Lescuyer},
title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
booktitle = {{AFM07 (Automated Formal Methods)}},
year = 2007,
month = {NOV},
address = {Atlanta, Georgia, USA},
editor = {John Rushby and N. Shankar},
abstract = {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.},
topics = {team,lri},
type_publi = {colloque},
url = {http://www.lri.fr/~kanig/publis/cckl-afm07.pdf}
}
@inproceedings{conchonsmt07,
author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig},
title = {{CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers}},
booktitle = {5th International Workshop on Satisfiability Modulo},
year = 2007,
month = jul,
address = {Berlin, Germany},
topics = {team, lri},
abstract = {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.},
url = {http://www.lri.fr/~kanig/publis/cck-smt07.ps}
}
This file was generated by bibtex2html 1.94.