@INPROCEEDINGS{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean
and St\'ephane Lescuyer},
title = {{Implementing Polymorphism in SMT solvers}},
booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
year = 2008,
editor = {Clark Barrett and Leonardo de Moura},
url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
abstract = { Based on our experience with the development of
Alt-Ergo, we show a small number of modifications needed to bring
parametric polymorphism to our SMT solver. The first one occurs in
the typing module where unification is now necessary for solving
polymorphic constraints over types. The second one consists in
extending triggers' definition in order to deal with both term and
type variables. Last, the matching module must be modified to
account for the instantiation of type variables. We hope that this
experience is convincing enough to raise interest for polymorphism
in the SMT community. }
}
@ARTICLE{conchon-entcs-08,
author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
title = {CC(X): Semantic Combination of Congruence Closure with Solvable Theories},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {198},
month = {May},
year = {2008},
pages = {51-69},
number = {2},
url = {http://www.lri.fr/~conchon/publis/conchon-entcs08.pdf},
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 semantic values for class representatives instead of canonized
terms. Using semantic 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
semantic values. CC(X) has been implemented in Ocaml and is at
the core of Ergo, a new automated theorem prover dedicated to
program verification.}
}
@INPROCEEDINGS{conchon07afm,
author = {Sylvain Conchon and Evelyne Contejean and Johannes Kannig and St{\'e}phane Lescuyer},
title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
booktitle = {{AFM07 (Automated Formal Methods)}},
year = 2007,
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.}
}
@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,
address = {Berlin, Germany},
month = JUL,
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.}
}
@MISC{ergo06,
author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig},
title = {{Ergo : a theorem prover for polymorphic first-order logic
modulo theories}},
year = 2006,
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 and a built-in theory
X. Its architecture is highly modular and it consists only of 3000
lines of Ocaml code. It is currently used to prove correctness of
C and Java programs.},
url = {http://ergo.lri.fr/papers/ergo.ps}
}
This file has been generated by bibtex2html 1.85.