Publications : Johannes Kanig
Back[14] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Journal of Automated Reasoning, 56(4):387457, 2016.
[ bib 
full text on HAL ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of builtin theories such as congruence, linear arithmetic, arrays, and bitvectors. 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 firstorder 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 firstorder logic and are included in the SMTLIB 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 onetime 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 AltErgo 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 featurerich axiomatization of doublylinked 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 doublylinked lists.

[13]  Claude Marché and Johannes Kanig. Bridging the gap between testing and formal verification in Ada development. ERCIM News, 100:3839, January 2015. [ bib  full text on HAL ] 
[12] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Submitted, 2013.
[ bib 
full text on HAL 
.pdf ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of builtin theories such as congruence, linear arithmetic, arrays, and bitvectors. 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 firstorder 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 firstorder logic and are included in the SMTLIB 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 onetime 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 AltErgo 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 featurerich axiomatization of doublylinked 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 doublylinked lists.

[11] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR7986, INRIA, June 2012.
[ bib 
full text on HAL 
.pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of builtin theories. Adding a builtin 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 firstorder 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 firstorder 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 
[10]  Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. LORIA. [ bib ] 
[9]  Johannes Kanig, Edmond Schonberg, and Claire Dross. HiLite: the convergence of compiler technology and program verification. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pages 2734, Boston, USA, 2012. ACM Press. [ bib ] 
[8]  Johannes Kanig. Spécification et preuve de programmes d'ordre supérieur. Thèse de doctorat, Université ParisSud, 2010. [ bib ] 
[7] 
Johannes Kanig and JeanChristophe Filliâtre.
Who: A Verifier for Effectful Higherorder Programs.
In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August
2009.
[ bib 
full text on HAL 
.pdf ]
We present Who, a tool for verifying effectful higherorder functions. It features Effect polymorphism, higherorder 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 MLlike programming languages.

[6] 
Romain Bardou, JeanChristophe Filliâtre, Johannes Kanig, and Stéphane
Lescuyer.
Faire bonne figure avec Mlpost.
In Vingtièmes Journées Francophones des Langages
Applicatifs, SaintQuentin sur Isère, January 2009. INRIA.
[ bib 
.pdf ]
Cet article présente Mlpost, une bibliothèque Ocaml de dessin scientifique. Elle s'appuie sur Metapost, qui permet notamment d'inclure des fragments L^{A}T_{E}X dans les figures. Ocaml offre une alternative séduisante aux langages de macros L^{A}T_{E}X, aux langages spécialisés ou même aux outils graphiques. En particulier, l'utilisateur de Mlpost bénéficie de toute l'expressivité d'Ocaml et de son typage statique. Enfin Mlpost propose un style déclaratif qui diffère de celui, souvent impératif, des outils existants.

[5] 
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
theories.
In Postproceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198(2) of
Electronic Notes in Computer Science, pages 5169. Elsevier Science
Publishers, 2008.
[ bib 
DOI ]
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 builtin solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a unionfind datastructure 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.

[4] 
Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer.
SATMICRO : petit mais costaud !
In Dixneuvièmes Journées Francophones des Langages
Applicatifs, Étretat, France, January 2008. INRIA.
[ bib 
.ps ]
Le problème SAT, qui consiste `a déterminer si une formule booléenne est satisfaisable, est un des problèmes NPcomplets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SATsolvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière nonchronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en Ocaml d'un SATsolver, baptisé SATMICRO, intégrant ces optimisations. Le fonctionnement de SATMICRO est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.

[3]  Johannes Kanig. Certifying a congruence closure algorithm in Coq using traces. Diplomarbeit, Technische Universität Dresden, April 2007. [ bib ] 
[2] 
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane
Lescuyer.
Lightweight Integration of the Ergo Theorem Prover inside a Proof
Assistant.
In John Rushby and N. Shankar, editors, Proceedings of the
second workshop on Automated formal methods, pages 5559. ACM Press, 2007.
[ bib 
DOI 
PDF 
.pdf ]
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 builtin 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.

[1]  Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. CC(X): Efficiently combining equality and solvable theories without canonizers. In Sava Krstic and Albert Oliveras, editors, SMT 2007: 5th International Workshop on Satisfiability Modulo, 2007. [ bib ] 
Back
This page was generated by bibtex2html.