kanig.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc kanig.cite -ob kanig.bib -c 'author : "kanig"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{boogie11hilite,
author = {J\'er\^ome Guitton and Johannes Kanig and Yannick Moy},
title = {{Why Hi-Lite Ada?}},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
pages = {27--39}
}
@inproceedings{boogie11hilite-short,
author = {J\'er\^ome Guitton and Johannes Kanig and Yannick Moy},
title = {{Why Hi-Lite Ada?}},
booktitle = {Boogie},
year = 2011,
pages = {27--39}
}
@inproceedings{hilite_erts,
author = {Cyrille Comar and Johannes Kanig and Yannick Moy},
title = {Integrating Formal Program Verification with Testing},
booktitle = {Proceedings of the Embedded Real Time Software and Systems conference},
series = {ERTS$^2$ 2012},
year = 2012,
location = {Toulouse, France},
month = feb,
keywords = {GNATprove}
}
@inproceedings{kanig14tap,
title = {Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification},
author = {Kanig, Johannes and Chapman, Rod and Comar, Cyrille and Guitton, Jerôme and Moy, Yannick and Rees, Emyr},
year = 2014,
booktitle = {Tests and Proofs, 8th International Conference},
volume = 8570,
series = {Lecture Notes in Computer Science},
editor = {Seidl, Martina and Tillmann, Nikolai},
doi = {10.1007/978-3-319-09099-3_11},
publisher = {Springer},
pages = {142--157}
}
@inproceedings{dross20cav,
author = {Claire Dross and Johannes Kanig},
title = {Recursive Data Structures in SPARK},
booktitle = {Computer Aided Verification},
year = 2020
}
@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{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.}
}
@mastersthesis{kanig07master,
author = {Johannes Kanig},
title = {Certifying a Congruence Closure algorithm in {Coq} using Traces},
school = {Technische Universit\"at Dresden},
year = 2007,
topics = {team, lri},
month = apr,
type = {Diplomarbeit}
}
@inproceedings{mlpost09jfla,
author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
title = {{Faire bonne figure avec Mlpost}},
url = {http://www.lri.fr/~filliatr/ftp/publis/mlpost-fra.pdf},
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.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla09}
}
@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},
address = {Edinburgh, Scotland, UK},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
month = aug,
year = 2009,
url = {http://www.lri.fr/~filliatr/ftp/publis/wml09.pdf},
hal = {http://hal.inria.fr/hal-00777585},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
abstract = {We present Who, a tool for verifying effectful higher-order
functions. It features {\em 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.}
}
@phdthesis{kanig10these,
author = {Johannes Kanig},
title = {Sp\'ecification et preuve de programmes d'ordre sup\'erieur},
school = {Universit{\'e} Paris-Sud},
type = {Th{\`e}se de Doctorat},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {these},
topics = {team},
year = 2010
}
@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{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{kanig12hilt,
topics = {team},
author = {Johannes Kanig and Edmond Schonberg and Claire Dross},
title = {{Hi-Lite}: the convergence of compiler technology and program
verification},
pages = {27--34},
editor = {Ben Brosgol and Jeff Boleng and S. Tucker Taft},
booktitle = {Proceedings of the 2012 ACM Conference on High Integrity
Language Technology, HILT '12},
address = {Boston, USA},
publisher = {ACM Press},
year = 2012
}
@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}
}
@article{marche15ercim,
topics = {team},
hal = {http://hal.inria.fr/hal-01102242},
author = {Claude March\'e and Johannes Kanig},
title = {Bridging the Gap between Testing and Formal
Verification in {Ada} Development},
journal = {ERCIM News},
year = 2015,
volume = 100,
pages = {38--39},
month = jan
}
@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{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{jfla09,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2009,
booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Quentin sur Is\`ere},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@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}
}