Publications : Sylvain Conchon
Back[45] 
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.

[44]  Sylvain Conchon and JeanChristophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, September 2014. [ bib  full text on HAL  http ] 
[43]  Sylvain Conchon and Mohamed Iguernelala. Tuning the AltErgo SMT solver for B proof obligations. In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 8477 of Lecture Notes in Computer Science, pages 294297, Toulouse, France, June 2014. Springer. [ bib  DOI  full text on HAL ] 
[42]  Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In Vingtcinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib  full text on HAL ] 
[41] 
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Invariants for finite instances and beyond.
In FMCAD, pages 6168, Portland, Oregon, ÉtatsUnis,
October 2013.
[ bib 
DOI 
full text on HAL ]
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 stateoftheart 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 overapproximations 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.

[40]  Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco, Gilles Dowek, JeanChristophe Filliâtre, and Stéphane Gonnord. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Eyrolles, August 2013. [ bib  full text on HAL  http ] 
[39]  Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. In Vingtquatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib  full text on HAL ] 
[38] 
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.

[37]  Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A Collaborative Framework for NonLinear Integer Arithmetic Reasoning in AltErgo. 2013. [ bib  full text on HAL  http ] 
[36]  Sylvain Conchon. SMT Techniques and their Applications: from AltErgo to Cubicle. Thèse d'habilitation, Université ParisSud, December 2012. In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf. [ bib  .html ] 
[35]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation. Logical Methods in Computer Science, 8(3):129, September 2012. Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany, 2011. [ bib  DOI  full text on HAL  http ] 
[34] 
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Cubicle: A parallel SMTbased model checker for parameterized
systems.
In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV
2012: Proceedings of the 24th International Conference on Computer Aided
Verification, volume 7358 of Lecture Notes in Computer Science,
Berkeley, California, USA, July 2012. Springer.
[ bib 
full text on HAL ]
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 stateoftheart model checkers.

[33] 
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplexbased extension of FourierMotzkin for solving linear
integer arithmetic.
In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors,
IJCAR 2012: Proceedings of the 6th International Joint Conference on
Automated Reasoning, volume 7364 of Lecture Notes in Computer Science,
pages 6781, Manchester, UK, June 2012. Springer.
[ bib 
DOI 
full text on HAL ]
This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. OmegaTest) or by branching/cutting methods (branchandbound, branchandcut, 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 AltErgo theorem prover. Experimental results are promising and show that our approach is competitive with stateoftheart SMT solvers.

[32] 
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 
[31]  Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Builtin treatment of an axiomatic floatingpoint theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, pages 1221, Manchester, UK, 2012. LORIA. [ bib ] 
[30]  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 ] 
[29]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of Lecture Notes in Computer Science, pages 4559, Saarbrücken, Germany, April 2011. Springer. [ bib  DOI  full text on HAL  .pdf  Abstract ] 
[28]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib  PDF  .pdf  Abstract ] 
[27]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Andrei Voronkov, editor, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, Yogyakarta, Indonesia, October 2010. (short paper). [ bib ] 
[26]  Sylvain Conchon, JeanChristophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation tempsréel de programmes Caml. In Vingtetunièmes Journées Francophones des Langages Applicatifs, VieuxPort La Ciotat, France, January 2010. INRIA. [ bib  .pdf ] 
[25]  Stéphane Lescuyer and Sylvain Conchon. Improving Coq propositional reasoning using a lazy CNF conversion scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287303, Trento, Italy, September 2009. Springer. [ bib  DOI ] 
[24]  François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 15, 2008. [ bib  DOI  PDF  .pdf  Abstract ] 
[23]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Marco T. Morazán, editor, Trends in Functional Programming Volume 8: Selected Papers of the 8^{th} International Symposium on Trends in Functional Programming (TFP'07), New York, USA, volume 8. Intellect, 2008. [ bib ] 
[22] 
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.

[21] 
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.

[20]  Sylvain Conchon and JeanChristophe Filliâtre. SemiPersistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib  PDF  .pdf ] 
[19]  François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The AltErgo automated theorem prover, 2008. http://altergo.lri.fr/. [ bib ] 
[18]  Sylvain Conchon and Évelyne Contejean. The AltErgo automatic theorem prover. http://altergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000. [ bib  http ] 
[17]  Stéphane Lescuyer and Sylvain Conchon. A reflexive formalization of a SAT solver in Coq. In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008. [ bib ] 
[16] 
Sylvain Conchon and JeanChristophe Filliâtre.
A Persistent UnionFind Data Structure.
In ACM SIGPLAN Workshop on ML, pages 3745, Freiburg, Germany,
October 2007. ACM Press.
[ bib 
PDF 
.pdf ]
The problem of disjoint sets, also known as unionfind, 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 unionfind 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.

[15] 
Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles.
Designing a Generic Graph Library using ML Functors.
In Marco T. Morazán and Henrik Nilsson, editors, The Eighth
Symposium on Trends in Functional Programming, volume TRSHUCS2007041,
pages XII/113, New York, USA, April 2007. Seton Hall University.
[ bib 
.ps ]
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 structuresdirected 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 socalled functors.

[14]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Trends in Functional Programming (TFP'07), New York City, USA, April 2007. [ bib  PDF  .pdf ] 
[13] 
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.

[12]  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 ] 
[11] 
Sylvain Conchon and JeanChristophe Filliâtre.
UnionFind Persistant.
In Dixhuitièmes Journées Francophones des Langages
Applicatifs, pages 135149. INRIA, January 2007.
[ bib 
PDF 
.pdf ]
Le problème des classes disjointes, connu sous le nom de unionfind, consiste à maintenir dans une structure de données une partition d'un ensemble fini. Cette structure fournit deux opérations : une fonction find déterminant la classe d'un élément et une fonction union réunissant deux classes. Une solution optimale et impérative, due à Tarjan, est connue depuis longtemps.

[10]  Sylvain Conchon and JeanChristophe Filliâtre. TypeSafe Modular HashConsing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib  PDF  .pdf ] 
[9]  Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187210, 2006. Special Issue of TCS dedicated to a refereed selection of papers presented at TACAS'03. [ bib ] 
[8]  Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(12):87106, May 2005. [ bib ] 
[7]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 7994. INRIA, March 2005. [ bib  .ps.gz ] 
[6]  Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. In Franz Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE19), volume 2741 of Lecture Notes in Computer Science, Miami Beach, FL, USA, July 2003. Springer. [ bib  .ps.gz ] 
[5]  Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. In Proceedings of the 9th Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of Lecture Notes in Computer Science, pages 537553, Warsaw, Poland, April 2003. Springer. [ bib  .ps.gz ] 
[4]  Sylvain Conchon. Modular information flow analysis for process calculi. In Iliano Cervesato, editor, Proceedings of the Foundations of Computer Security Workshop (FCS 2002), Copenhagen, Denmark, July 2002. [ bib  .ps.gz ] 
[3]  Sylvain Conchon and François Pottier. JOIN(X): Constraintbased type inference for the joincalculus. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in Computer Science, pages 221236, Genova, Italy, April 2001. Springer. [ bib  .ps.gz ] 
[2]  François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pages 4657, Montréal, Canada, September 2000. [ bib  .ps.gz ] 
[1]  Sylvain Conchon and Fabrice Le Fessant. Jocaml: Mobile agents for ObjectiveCaml. In First International Symposium on Agent Systems and Applications and Third International Symposium on Mobile Agents (ASA/MA'99), pages 2229, Palm Springs, California, October 1999. [ bib  .ps.gz ] 
Back
This page was generated by bibtex2html.