conchon.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc conchon.cite -ob conchon.bib -c 'author : "conchon"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@techreport{conchon10rr,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
institution = {{LRI, Universit\'e Paris Sud}},
year = 2010,
type = {Research Report},
number = 1538,
month = dec,
topics = {team, lri},
type_publi = {interne},
type_digiteo = {no},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {rapport},
x-pdf = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
url = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
abstract = {http://www.lri.fr/~contejea/publis/rr1538/abstract.html}
}
@inproceedings{conchon11tacas,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
crossref = {tacas2011},
year = 2011,
month = apr,
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {TACAS},
url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
hal = {http://hal.inria.fr/hal-00777663},
pages = {45-59},
doi = {10.1007/978-3-642-19835-9_6},
abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@article{conchon12lmcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {Canonized Rewriting and Ground {AC} Completion Modulo {Shostak} Theories : Design and Implementation},
journal = {Logical Methods in Computer Science},
year = {2012},
month = sep,
pages = {1--29},
volume = 8,
number = 3,
hal = {http://hal.inria.fr/hal-00798082},
url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-international-audience = {yes},
x-editorial-board = {yes},
x-cle-support = {LMCS},
doi = {10.2168/LMCS-8(3:16)2012},
note = {Selected Papers of the Conference \emph{Tools and Algorithms for the Construction and Analysis of Systems} (TACAS 2011), Saarbr{\"u}cken, Germany, 2011}
}
@inproceedings{conchon10lpar,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Ground Associative and Commutative Completion Modulo Shostak Theories}},
booktitle = {LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = 2010,
editor = {Andrei Voronkov},
series = {EasyChair Proceedings},
address = {Yogyakarta, Indonesia},
month = oct,
note = {(short paper)},
type_publi = {colloque},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {LPAR}
}
@inproceedings{conchon-02,
author = {Sylvain Conchon},
title = {Modular Information Flow Analysis for Process Calculi},
booktitle = {Proceedings of the Foundations of Computer Security Workshop (FCS 2002)},
editor = {Iliano Cervesato},
month = jul,
address = {Copenhagen, Denmark},
year = {2002},
url = {http://www.lri.fr/~conchon/publis/conchon-fcs02.ps.gz},
topics = {team},
type_publi = {icolcomlec}
}
@article{conchon06tcs,
author = {Sylvain Conchon and Sava Krsti{\'c}},
title = {Strategies for Combining Decision Procedures},
journal = {Theoretical Computer Science},
year = 2006,
volume = 354,
number = 2,
pages = {187--210},
note = {Special Issue of TCS dedicated to a refereed
selection of papers presented at TACAS'03},
topics = {team,lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TCS}
}
@article{krstic-conchon-05,
author = {Sava Krsti{\'c} and Sylvain Conchon},
title = {Canonization for disjoint unions of theories},
journal = {Information and Computation},
volume = {199},
month = {May},
year = {2005},
pages = {87--106},
topics = {team},
number = {1-2},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {JIC}
}
@inproceedings{conchon-krstic-02,
author = {Sylvain Conchon and Sava Krsti{\'c}},
title = {Strategies for Combining Decision Procedures},
booktitle = {Proceedings of the 9th Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03)},
address = {Warsaw, Poland},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {537--553},
month = apr,
year = {2003},
url = {http://www.cse.ogi.edu/~conchon/publis/conchon-krstic.ps.gz},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
type_publi = {icolcomlec}
}
@inproceedings{krstic-conchon-02,
author = {Sava Krsti{\'c} and Sylvain Conchon},
title = {Canonization for Disjoint Unions of Theories},
booktitle = {Proceedings of the 19th International Conference on Automated Deduction
(CADE-19)},
editor = {Franz Baader},
address = {Miami Beach, FL, USA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2741},
month = jul,
year = {2003},
url = {http://www.lri.fr/~conchon/publis/krstic-conchon.ps.gz},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {CADE}
}
@inproceedings{conchon-le-fessant-99,
title = {Jocaml: Mobile Agents for {Objective-Caml}},
author = {Sylvain Conchon and Fabrice Le Fessant},
booktitle = {First International Symposium on Agent Systems and
Applications and Third International Symposium on
Mobile Agents (ASA/MA'99)},
address = {Palm Springs, California},
year = {1999},
month = oct,
pages = {22--29},
url = {http://www.lri.fr/~conchon/publis/conchon-lefessant-asama99.ps.gz},
topics = {team}
}
@inproceedings{conchon-pottier-01,
author = {Sylvain Conchon and Fran\c{c}ois Pottier},
title = {{JOIN(X)}: Constraint-Based Type Inference for the
Join-Calculus},
booktitle = {Proceedings of the 10th European Symposium on
Programming (ESOP'01)},
editor = {David Sands},
address = {Genova, Italy},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2028},
pages = {221--236},
month = apr,
year = {2001},
url = {http://www.lri.fr/~conchon/publis/conchon-fpottier-esop01.ps.gz},
topics = {team}
}
@inproceedings{conchon05jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
title = {Le foncteur sonne toujours deux fois},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla05},
pages = {79--94},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla05.ps.gz}
}
@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}},
crossref = {afm07},
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.},
abstract = {http://www.lri.fr/~contejea/publis/2007afm/abstract.html},
topics = {team,lri},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {AFM},
x-pdf = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
url = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
doi = {10.1145/1345169.1345176},
pages = {55--59}
}
@inproceedings{conchon07smt,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig},
title = {{CC(X)}: Efficiently Combining Equality and Solvable Theories without Canonizers},
booktitle = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
year = 2007,
editor = {Sava Krstic and Albert Oliveras},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT}
}
@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},
pages = {1--5},
year = 2008,
editor = {Clark Barrett and Leonardo de Moura},
volume = 367,
series = {ACM International Conference Proceedings Series},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT},
x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
isbn = {978-1-60558-440-9},
doi = {10.1145/1512464.1512466},
abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@inproceedings{conchon07tfp,
author = {Sylvain Conchon and
Jean-Christophe Filli\^atre and
Julien Signoles},
title = {{Designing a Generic Graph Library using {ML} Functors}},
booktitle = {The Eighth Symposium on Trends in Functional Programming},
editor = {Marco T. Moraz\'an and Henrik Nilsson},
publisher = {Seton Hall University},
volume = {TR-SHU-CS-2007-04-1},
pages = {XII/1--13},
year = 2007,
address = {New York, USA},
month = apr,
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
abstract = {
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
structures---directed 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 so-called
functors.},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp07.ps},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-editorial-board = {yes}
}
@incollection{conchon07tfpbook,
author = {Sylvain Conchon and
Jean-Christophe Filli\^atre and
Julien Signoles},
title = {{Designing a Generic Graph Library using ML Functors}},
booktitle = {Trends in Functional Programming Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP'07), New York, USA},
editor = {Marco T. Moraz\'an},
publisher = {Intellect},
year = 2008,
volume = 8,
isbn = {9781841501963},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {ouvrage},
x-cle-support = {TFP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{conchon08tfp,
author = {Sylvain Conchon and
Jean-Christophe Filli\^atre and
Julien Signoles},
title = {Designing a Generic Graph Library using {ML} Functors},
booktitle = {Trends in Functional Programming (TFP'07)},
month = {April},
year = 2007,
address = {New York City, USA},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {TFP},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@misc{conchonijcar06,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {Rule Based Incremental Congruence Closure with Commutative
Symbols},
month = mar,
year = 2006
}
@inproceedings{conchon08entcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
title = {{CC(X)}: Semantical Combination of Congruence Closure with
Solvable Theories},
booktitle = {Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories ({SMT 2007})},
series = {Electronic Notes in Computer Science},
publisher = {Elsevier Science Publishers},
volume = {198(2)},
pages = {51--69},
year = 2008,
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.
},
abstract = {http://www.lri.fr/~contejea/publis/2008entcs/abstract.html},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {ENTCS},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
doi = {10.1016/j.entcs.2008.04.080}
}
@inproceedings{Conchon08jfla,
author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
title = {{SAT-MICRO : petit mais costaud !}},
year = 2008,
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
x-editorial-board = {yes},
x-international-audience = {no},
x-proceedings = {yes},
crossref = {jfla08},
address = {\'Etretat, France},
publisher = {INRIA},
url = {http://www.lri.fr/~conchon/publis/conchon-jfla08.ps},
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. 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.}
}
@inproceedings{ConchonFilliatre06wml,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Type-Safe Modular Hash-Consing}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
month = sep,
year = 2006,
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre07jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Union-Find Persistant}},
year = 2007,
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla07},
pages = {135--149},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
abstract = {
Le probl\`eme des classes disjointes, connu sous le nom de
\emph{union-find}, consiste \`a maintenir dans une structure de
donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
op\'erations : une fonction \emph{find} d\'eterminant la classe d'un
\'el\'ement et une fonction \emph{union} r\'eunissant deux classes. Une
solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
longtemps.
Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
s'effectuent des retours en arri\`ere (\emph{backtracking}). Nous
pr\'esentons dans cet article une version persistante de
\emph{union-find} dont la complexit\'e est comparable \`a celle de la
solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
utilise massivement des traits imp\'eratifs. C'est pourquoi nous
pr\'esentons \'egalement une preuve formelle de correction, pour
s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@techreport{ConchonFilliatre07rr,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {Semi-Persistent Data Structures}
}
@inproceedings{ConchonFilliatre07wml,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{A Persistent Union-Find Data Structure}},
booktitle = {ACM SIGPLAN Workshop on ML},
publisher = {ACM Press},
pages = {37--45},
year = 2007,
address = {Freiburg, Germany},
month = {October},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
abstract = { The problem of disjoint sets, also known as union-find,
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 union-find 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. },
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre08esop,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
hal = {https://inria.hal.science/hal-04045849},
doi = {10.1007/978-3-540-78739-6_25},
title = {Semi-Persistent Data Structures},
crossref = {esop08},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-url = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@misc{alt-ergo,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
title = {The {Alt-Ergo} Automated Theorem Prover},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL}
}
@misc{ergo,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {The {Alt-Ergo} automatic Theorem Prover},
url = {http://alt-ergo.lri.fr/},
howpublished = {\url{http://alt-ergo.lri.fr/}},
note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@misc{altergo10app,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {Alt-Ergo},
howpublished = {APP Deposit},
month = mar,
year = 2010,
note = {IDDN.FR.001.110026.000.S.P.2010.000.10000},
annote = {\url{http://alt-ergo.lri.fr}}
}
@inproceedings{pottier-conchon-icfp-00,
author = {Fran\c{c}ois Pottier and Sylvain Conchon},
title = {Information Flow Inference for Free},
booktitle = {Proceedings of the Fifth {ACM} {SIGPLAN}
International Conference on Functional Programming (ICFP'00)},
url = {http://www.cse.ogi.edu/~conchon/publis/fpottier-conchon-icfp00.ps.gz},
month = sep,
year = {2000},
pages = {46--57},
address = {Montr\'eal, Canada},
topics = {team}
}
@inproceedings{lescuyer08tpholset,
author = {St\'ephane Lescuyer and Sylvain Conchon},
title = {A Reflexive Formalization of a {SAT} Solver in {Coq}},
booktitle = {Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics},
year = 2008,
topics = {team},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {?},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{LescuyerConchon09frocos,
author = {St{\'e}phane Lescuyer and Sylvain Conchon},
title = {Improving {Coq} Propositional Reasoning using a Lazy {CNF} Conversion Scheme},
topics = {team},
x-support = {actes},
pages = {287-303},
doi = {10.1007/978-3-642-04222-5_18},
crossref = {frocos09}
}
@inproceedings{conchon10jfla,
author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe
and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
title = {{Observation temps-r\'eel de programmes Caml}},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10},
url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf}
}
@inproceedings{conchon12cav,
author = {Sylvain Conchon and Amit Goel and Sava Krsti{\'c}
and Alain Mebsout and Fatiha Za{\"i}di},
title = {{Cubicle}: A Parallel {SMT}-based Model Checker for
Parameterized Systems},
booktitle = {CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification},
year = {2012},
topics = {team},
hal = {http://hal.archives-ouvertes.fr/hal-00799272},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL Fortesse ext},
x-type = {article},
x-support = {actes},
x-cle-support = {CAV},
editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
series = {Lecture Notes in Computer Science},
volume = 7358,
month = jul,
address = {Berkeley, California, USA},
publisher = {Springer},
abstract = { Cubicle is a new model checker for verifying safety
properties of parameterized systems. It implements a
parallel symbolic backward reachability procedure
using Satisfiabilty Modulo Theories. Experiments
done on classic and challenging mutual exclusion
algorithms and cache coherence protocols show that
Cubicle is effective and competitive with
state-of-the-art model checkers.}
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {This paper describes a novel decision procedure for
quantifier-free linear integer arithmetic. Standard
techniques usually relax the initial problem to the
rational domain and then proceed either by
projection (e.g. Omega-Test) or by branching/cutting
methods (branch-and-bound, branch-and-cut, Gomory
cuts). Our approach tries to bridge the gap between
the two techniques: it interleaves an exhaustive
search for a model with bounds inference. These
bounds are computed provided an oracle capable of
finding constant positive linear combinations of
affine forms. We also show how to design an
efficient oracle based on the Simplex procedure. Our
algorithm is proved sound, complete, and terminating
and is implemented in the Alt-Ergo theorem
prover. Experimental results are promising and show
that our approach is competitive with
state-of-the-art SMT solvers.}
}
@techreport{dross12rr,
title = {Reasoning with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
and Paskevich, Andrei},
abstract = {SMT solvers can decide the satisfiability of ground
formulas modulo a combination of built-in
theories. Adding a built-in theory to a given SMT
solver is a complex and time consuming task that
requires internal knowledge of the solver. However,
many theories can be easily expressed using
first-order formulas. Unfortunately, since universal
quantifiers are not handled in a complete way by SMT
solvers, these axiomatics cannot be used as decision
procedures. In this paper, we show how to extend a
generic SMT solver to accept a custom theory
description and behave as a decision procedure for
that theory, provided that the described theory is
complete and terminating in a precise sense. The
description language consists of first-order axioms
with triggers, an instantiation mechanism that is
found in many SMT solvers. This mechanism, which
usually lacks a clear semantics in existing
languages and tools, is rigorously defined here;
this definition can be used to prove completeness
and termination of the theory. We demonstrate on two
examples, how such proofs can be achieved in our
formalism.},
keywords = {Quantifiers, Triggers, SMT Solvers, Theories},
language = {English},
affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI},
pages = 29,
type = {Research Report},
institution = {INRIA},
number = {RR-7986},
year = 2012,
month = jun,
x-equipes = {demons PROVAL ext},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/hal-00703207},
pdf = {http://hal.inria.fr/hal-00703207/PDF/RR-7986.pdf}
}
@inproceedings{conchon12smt,
author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
pages = {12--21},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-cle-support = {SMT},
x-type = {article},
crossref = {smt2012},
topics = {team}
}
@inproceedings{dross12smt,
author = {Claire Dross and Sylvain Conchon and Johannes Kanig and Andrei Paskevich},
title = {Reasoning with Triggers},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
x-cle-support = {SMT},
crossref = {smt2012},
topics = {team}
}
@inproceedings{conchon13jfla,
author = {Sylvain Conchon and Alain Mebsout and Fatiha Za\"{\i}di},
title = {V\'erification de syst\`emes param\'etr\'es avec {Cubicle}},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL Fortesse},
x-type = {article},
x-support = {actes},
hal = {http://hal.inria.fr/hal-00778832}
}
@phdthesis{conchon12hdr,
author = {Sylvain Conchon},
title = {{SMT} Techniques and their Applications: from {Alt-Ergo} to {Cubicle}},
year = 2012,
month = dec,
type = {Th\`{e}se d'habilitation},
school = {Universit{\'e} Paris-Sud},
type_publi = {these},
url = {http://www.lri.fr/~conchon/bib/conchon.html},
note = {In English, \url{http://www.lri.fr/~conchon/publis/conchonHDR.pdf}},
rawebnote = {In English, \url{http://www.lri.fr/~conchon/publis/conchonHDR.pdf}},
x-equipes = {demons PROVAL},
x-type = {habilitation},
x-support = {rapport},
topics = {team}
}
@book{InfoPourTous2013Eyrolles,
hal = {http://hal.inria.fr/hal-00880268},
topics = {team},
author = {Benjamin Wack and Sylvain Conchon and Judica\"el Courant and Marc de Falco and Gilles Dowek and Jean-Christophe Filli\^atre and St\'ephane Gonnord},
title = {Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python},
publisher = {Eyrolles},
year = 2013,
month = aug,
pages = 408,
url = {http://www.eyrolles.com/Sciences/Livre/informatique-pour-tous-en-classes-preparatoires-aux-grandes-ecoles-9782212137002},
isbn = 2212137001,
x-equipes = {demons PROVAL EXT},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage}
}
@unpublished{dross13,
topics = {team},
hal = {http://hal.inria.fr/hal-00915931},
title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
abstract = {SMT solvers are efficient tools to decide the
satisfiability of ground formulas, including a
number of built-in theories such as congruence,
linear arithmetic, arrays, and bit-vectors. Adding a
theory to that list requires delving into the
implementation details of a given SMT solver, and is
done mainly by the developers of the solver
itself. For many useful theories, one can
alternatively provide a first-order
axiomatization. However, in the presence of
quantifiers, SMT solvers are incomplete and exhibit
unpredictable behavior. Consequently, this approach
can not provide us with a complete and terminating
treatment of the theory of interest. In this paper,
we propose a framework to solve this problem, based
on the notion of instantiation patterns, also known
as triggers. Triggers are annotations that suggest
instances which are more likely to be useful in
proof search. They are implemented in all SMT
solvers that handle first-order logic and are
included in the SMT-LIB format. In our framework,
the user provides a theory axiomatization with
triggers, along with a proof of completeness and
termination properties of this axiomatization, and
obtains a sound, complete, and terminating solver
for her theory in return. We describe and prove a
corresponding extension of the traditional Abstract
DPLL Modulo Theory framework. Implementing this
mechanism in a given SMT solver requires a one-time
development effort. We believe that this effort is
not greater than that of adding a single decision
procedure to the same SMT solver. We have
implemented the proposed extension in the Alt-Ergo
prover and we discuss some implementation details in
the paper. To show that our framework can handle
complex theories, we prove completeness and
termination of a feature-rich axiomatization of
doubly-linked lists. Our tests show that our
approach results in a better performance of the
solver on goals that stem from the verification of
programs manipulating doubly-linked lists.},
language = {Anglais},
affiliation = {TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , AdaCore SAS - AdaCore SAS},
year = 2013,
pdf = {http://hal.inria.fr/hal-00915931/PDF/dross-article.pdf},
note = {Submitted}
}
@article{dross16jar,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01221066},
title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
abstract = {SMT solvers are efficient tools to decide the
satisfiability of ground formulas, including a
number of built-in theories such as congruence,
linear arithmetic, arrays, and bit-vectors. Adding a
theory to that list requires delving into the
implementation details of a given SMT solver, and is
done mainly by the developers of the solver
itself. For many useful theories, one can
alternatively provide a first-order
axiomatization. However, in the presence of
quantifiers, SMT solvers are incomplete and exhibit
unpredictable behavior. Consequently, this approach
can not provide us with a complete and terminating
treatment of the theory of interest. In this paper,
we propose a framework to solve this problem, based
on the notion of instantiation patterns, also known
as triggers. Triggers are annotations that suggest
instances which are more likely to be useful in
proof search. They are implemented in all SMT
solvers that handle first-order logic and are
included in the SMT-LIB format. In our framework,
the user provides a theory axiomatization with
triggers, along with a proof of completeness and
termination properties of this axiomatization, and
obtains a sound, complete, and terminating solver
for her theory in return. We describe and prove a
corresponding extension of the traditional Abstract
DPLL Modulo Theory framework. Implementing this
mechanism in a given SMT solver requires a one-time
development effort. We believe that this effort is
not greater than that of adding a single decision
procedure to the same SMT solver. We have
implemented the proposed extension in the Alt-Ergo
prover and we discuss some implementation details in
the paper. To show that our framework can handle
complex theories, we prove completeness and
termination of a feature-rich axiomatization of
doubly-linked lists. Our tests show that our
approach results in a better performance of the
solver on goals that stem from the verification of
programs manipulating doubly-linked lists.},
year = 2016,
journal = {Journal of Automated Reasoning},
volume = 56,
number = 4,
pages = {387--457}
}
@inproceedings{conchon14abz,
topics = {team},
hal = {https://hal.inria.fr/hal-01093000},
author = {Sylvain Conchon and Mohamed Iguernelala},
title = {Tuning the {Alt-Ergo} {SMT} Solver for {B} Proof Obligations},
pages = {294--297},
year = 2014,
crossref = {abz2014},
doi = {10.1007/978-3-662-43652-3_27}
}
@book{ProgrammerOCaml2014Eyrolles,
topics = {team},
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {Apprendre \`a programmer avec OCaml. Algorithmes et structures de donn\'ees},
publisher = {Eyrolles},
year = 2014,
month = sep,
pages = 429,
url = {https://usr.lmf.cnrs.fr/programmer-avec-ocaml/},
isbn = 9782212136784,
x-equipes = {demons PROVAL},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage},
hal = {http://hal.inria.fr/hal-01063853}
}
@inproceedings{conchon13fmcad,
topics = {team},
hal = {http://hal.archives-ouvertes.fr/hal-00924640},
title = {Invariants for Finite Instances and Beyond},
author = {Conchon, Sylvain and Goel, Amit and Krsti{\'c}, Sava and Mebsout, Alain and Za{\"\i}di, Fatiha},
abstract = {Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.},
booktitle = {FMCAD},
pages = {61--68},
address = {Portland, Oregon, {\'E}tats-Unis},
audience = {internationale},
doi = {10.1109/FMCAD.2013.6679392},
year = 2013,
month = oct
}
@inproceedings{conchon14jfla,
hal = {https://hal.inria.fr/hal-01088655},
topics = {team},
author = {Sylvain Conchon and David Declerck and Luc Maranget and Alain Mebsout},
title = {Vérification de programmes {C} concurrents avec {Cubicle} : Enfoncer les barrières},
crossref = {jfla14}
}
@unpublished{conchon:hal-00924646,
title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in {Alt-Ergo}},
author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
year = 2013,
hal = {https://hal.archives-ouvertes.fr/hal-00924646}
}
@inproceedings{conchon13synasc,
topics = {team},
author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo},
year = 2013,
doi = {10.1109/SYNASC.2013.29},
booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
pages = {161--168}
}
@inproceedings{conchon17cav,
author = {Sylvain Conchon and Mohamed Iguernlala and Kailiang Ji and
Guillaume Melquiond and Cl\'ement Fumex},
topics = {team},
hal = {https://hal.inria.fr/hal-01522770},
title = {A Three-tier Strategy for Reasoning about
Floating-Point Numbers in {SMT}},
booktitle = {Computer Aided Verification},
year = 2017,
pages = {419--435},
series = {Lecture Notes in Computer Science},
volume = 10427,
doi = {10.1007/978-3-319-63390-9_22}
}
@inproceedings{conchon17icfem,
topics = {team},
author = {Conchon, Sylvain and Declerck, David and Za{\"i}di, Fatiha},
editor = {Duan, Zhenhua and Ong, Luke},
title = {Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-W},
booktitle = {International Conference on Formal Engineering Methods},
year = 2017,
series = {Lecture Notes in Computer Science},
number = 10610,
pages = {88--104}
}
@inproceedings{roux18tacas,
topics = {team},
title = {A Non-linear Arithmetic Procedure for Control-Command Software Verification},
author = {Roux, Pierre and Iguernlala, Mohamed and Conchon, Sylvain},
hal = {https://hal.archives-ouvertes.fr/hal-01737737},
booktitle = {24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
address = {Thessalonique, Greece},
year = 2018,
month = apr
}
@inproceedings{conchon17fmcad,
topics = {team},
hal = {https://hal.inria.fr/hal-01927220},
author = {Sylvain Conchon and
Amit Goel and
Sava Krstic and
Rupak Majumdar and
Mattias Roux},
title = {{FAR-Cubicle} - {A} new reachability algorithm for {Cubicle}},
booktitle = {Formal Methods in Computer Aided Design},
pages = {172--175},
year = 2017,
doi = {10.23919/FMCAD.2017.8102256},
editor = {Daryl Stewart and Georg Weissenbacher}
}
@book{NSIPremiere2019Ellipses,
author = {Thibaut Balabonski and Sylvain Conchon and Jean-Christophe Filli\^atre and Kim Nguyen},
title = {Num\'erique et Sciences Informatiques, 30 le\c{c}ons avec exercices corrig\'es},
publisher = {Ellipses},
year = 2019,
month = aug,
pages = 528,
url = {http://www.nsi-premiere.fr},
isbn = 9782340033641,
x-equipes = {demons PROVAL},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage}
}
@inproceedings{conchon18smt,
topics = {team},
title = {{Alt-Ergo} 2.2},
author = {Conchon, Sylvain and Coquereau, Albin and Iguernlala, Mohamed and Mebsout, Alain},
hal = {https://hal.inria.fr/hal-01960203},
booktitle = {SMT Workshop: International Workshop on Satisfiability Modulo Theories},
address = {Oxford, United Kingdom},
year = 2018,
month = jul,
pdf = {https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf},
hal_id = {hal-01960203},
hal_version = {v1}
}
@inproceedings{conchon19icfem,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-02420588},
author = {Sylvain Conchon and Mattias Roux},
title = {Reasoning About Universal Cubes in {MCMT}},
booktitle = {International Conference on Formal Engineering Methods},
pages = {270--285},
editor = {Yamine A{\"{\i}}t Ameur and Shengchao Qin},
series = {Lecture Notes in Computer Science},
volume = 11852,
publisher = {Springer},
year = 2019
}
@inproceedings{conchon18ijcar,
topics = {team},
hal = {https://hal.inria.fr/hal-02420590},
author = {Sylvain Conchon and David Declerck and Fatiha Za{\"{\i}}di},
title = {Cubicle-W : Parameterized Model Checking on Weak Memory},
booktitle = {International Joint Conference on Automated Reasoning},
pages = {152--160},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
series = {Lecture Notes in Computer Science},
volume = 10900,
publisher = {Springer},
year = 2018
}
@inproceedings{conchon18netsy,
topics = {team},
hal = {https://hal.inria.fr/hal-02001652},
author = {Sylvain Conchon and
Giorgio Delzanno and
Angelo Ferrando},
title = {Declarative Parameterized Verification of Topology-Sensitive Distributed
Protocols},
pages = {209--224},
year = 2018,
editor = {Andreas Podelski and
Fran{\c{c}}ois Ta{\"{\i}}ani},
booktitle = {Networked Systems, 6th International Conference, Revised Selected Papers},
series = {Lecture Notes in Computer Science}
}
@article{conchon20jar,
topics = {team},
title = {Parameterized Model Checking on the {TSO} Weak Memory Model},
author = {Conchon, Sylvain and Declerck, David and Za{\"i}di, Fatiha},
hal = {https://hal.inria.fr/hal-03149332},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 64,
number = 7,
pages = {1307--1330},
year = 2020
}
@inproceedings{lecomte20erts,
topics = {team},
title = {Low Cost High Integrity Platform},
author = {Lecomte, Thierry and D{\'e}harbe, David and Sabatier, Denis and Prun, Etienne and P{\'e}ronne, Patrick and Chailloux, Emmanuel and Varoumas, Steven and Susungi, Adilla and Conchon, Sylvain},
hal = {https://hal.archives-ouvertes.fr/hal-02446132},
booktitle = {10th European Congress on Embedded Real Time Systems (ERTS)},
address = {Toulouse, France},
year = 2020,
keywords = {Safety ; Certification ; Formal methods}
}
@book{balabonski20book,
topics = {team},
title = {Num{\'e}rique et Sciences Informatiques, 24 le\c{c}ons avec exercices corrig{\'e}s. Terminale},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
hal = {https://hal.inria.fr/hal-03023099},
publisher = {Ellipses},
year = 2020
}
@book{balabonski22book,
topics = {team},
title = {Informatique - {MP2I/MPI} - {CPGE} 1re et 2e ann{\'e}es - {Cours} et exercices corrig{\'e}s},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim and Sartre, Laurent},
hal = {https://hal.inria.fr/hal-03886751},
publisher = {Ellipses},
year = 2022
}
@book{balabonski19book,
topics = {team},
title = {Num{\'e}rique et Sciences Informatiques, 30 le{\c c}ons avec exercices corrig{\'e}s. {Premi{\`e}re.}},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
hal = {https://inria.hal.science/hal-02379073},
publisher = {Ellipses},
year = 2019
}
@inproceedings{bozman22jfla,
topics = {team},
title = {Jouez {\`a} Faire Consensus Avec {MITTEN} (d{\'e}monstration)},
author = {Bozman, {\c C}agdas and Iguernlala, Mohamed and Laporte, Michael and Levillain, Maxime and Mebsout, Alain and Conchon, Sylvain},
hal = {https://hal.inria.fr/hal-03626847},
booktitle = {33{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Chantal Keller and Timothy Bourke},
pages = {248--250},
year = 2022
}
@inproceedings{conchon21iccl,
topics = {team},
author = {Sylvain Conchon and Giorgio Delzanno and Arnaud Sangnier},
editor = {Stefania Monica and Federico Bergenti},
title = {Verification of Contact Tracing Protocols via SMT-based Model Checking
and Counting Abstraction},
booktitle = {Proceedings of the 36th Italian Conference on Computational Logic,
Parma, Italy, September 7-9, 2021},
series = {{CEUR} Workshop Proceedings},
volume = 3002,
pages = {77--91},
publisher = {CEUR-WS.org},
year = 2021,
url = {https://ceur-ws.org/Vol-3002/paper24.pdf}
}
@inproceedings{conchon21fmbc,
topics = {team},
author = {Sylvain Conchon and Alexandrina Korneva and {\c{C}}agdas Bozman and
Mohamed Iguernlala and Alain Mebsout},
editor = {Bruno Bernardo and Diego Marmsoler},
title = {Formally Documenting Tenderbake (Short Paper)},
booktitle = {3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV
2021, July 18-19, 2021, Los Angeles, California, {USA} (Virtual Conference)},
series = {OASIcs},
volume = 95,
pages = {4:1--4:9},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = 2021,
doi = {10.4230/OASICS.FMBC.2021.4}
}
@article{conchon21fi,
topics = {team},
author = {Sylvain Conchon and Giorgio Delzanno and Angelo Ferrando},
title = {Declarative Parameterized Verification of Distributed Protocols via
the Cubicle Model Checker},
journal = {Fundam. Informaticae},
volume = 178,
number = 4,
pages = {347--378},
year = 2021,
doi = {10.3233/FI-2021-2010}
}
@inproceedings{conchon22fab,
topics = {team},
author = {Sylvain Conchon},
editor = {Sara Tucci Piergiovanni and Natacha Crooks},
title = {Some Insights on Open Problems in Blockchains: Explorative Tracks
for Tezos (Invited Talk)},
booktitle = {5th International Symposium on Foundations and Applications of Blockchain
2022, {FAB} 2022, June 3, 2022, Berkeley, CA, {USA}},
series = {OASIcs},
volume = 101,
pages = {2:1--2:1},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = 2022,
doi = {10.4230/OASICS.FAB.2022.2}
}
@inproceedings{conchon23sefm,
topics = {team},
hal = {https://inria.hal.science/hal-04394062},
author = {Sylvain Conchon and Alexandrina Korneva},
editor = {Carla Ferreira and Tim A. C. Willemse},
title = {The Cubicle Fuzzy Loop: {A} Fuzzing-Based Extension for the {Cubicle}
Model Checker},
booktitle = {Software Engineering and Formal Method},
series = {Lecture Notes in Computer Science},
volume = 14323,
pages = {30--46},
publisher = {Springer},
year = 2023,
doi = {10.1007/978-3-031-47115-5\_3}
}
@proceedings{afm07,
title = {{Proceedings of the second workshop on Automated formal methods}},
booktitle = {{Proceedings of the second workshop on Automated formal methods}},
year = 2007,
editor = {John Rushby and N. Shankar},
publisher = {ACM Press},
isbn = {978-1-59593-879-4}
}
@proceedings{tacas2011,
title = {Tools and Algorithms for the Construction and Analysis of Systems},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
year = 2011,
month = apr,
editor = {Parosh A. Abdulla and K. Rustan M. Leino},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
isbn = {978-3-642-19834-2},
address = {Saarbr{\"u}cken, Germany}
}
@proceedings{jfla05,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2005,
booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = mar,
publisher = {INRIA}
}
@proceedings{jfla07,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2007,
booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla08,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2008,
booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla10,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2010,
booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Vieux-Port La Ciotat, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla13,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2013,
booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Aussois, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla14,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2014,
booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Fr\'ejus, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{frocos09,
editor = {Silvio Ghilardi and
Roberto Sebastiani},
title = {Frontiers of Combining Systems, 7th International Symposium,
FroCoS 2009, Proceedings},
booktitle = {Frontiers of Combining Systems, 7th International Symposium, Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5749},
year = {2009},
month = sep,
address = {Trento, Italy},
isbn = {978-3-642-04221-8},
doi = {http://dx.doi.org/10.1007/978-3-642-04222-5},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{esop08,
title = {17th European Symposium on Programming (ESOP'08)},
booktitle = {17th European Symposium on Programming (ESOP'08)},
year = 2008,
address = {Budapest, Hungary},
month = apr
}
@proceedings{smt2012,
booktitle = {SMT workshop},
editor = {Pascal Fontaine and Amit Goel},
publisher = {LORIA},
url = {http://smt2012.loria.fr/},
year = 2012,
x-international-audience = {yes},
x-proceedings = {no},
address = {Manchester, UK}
}
@proceedings{abz2014,
booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
publisher = {Springer},
address = {Toulouse, France},
volume = 8477,
series = {Lecture Notes in Computer Science},
audience = {internationale},
year = 2014,
month = jun
}