kanig.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc kanig.cite -ob kanig.bib -c 'author : "kanig" and topics : "team"' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}
@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 = {http://dx.doi.org/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 = {http://dx.doi.org/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},
  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,
  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},
  crossref = {smt2012},
  topics = {team}
}
@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 = {\url{http://smt2012.loria.fr/}},
  year = 2012,
  address = {Manchester, UK}
}