The ProVal team was stopped at the end of August 2012, and reborn into a new team
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Publications : Sylvain ConchonBack
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Cubicle: A parallel SMT-based model checker for parameterized
In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV
2012: Proceedings of the 24th International Conference on Computer Aided
Verification, Lecture Notes in Computer Science, Berkeley, California, USA,
July 2012. Springer.
[ bib ]
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.
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplex-based extension of Fourier-Motzkin for solving linear
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 67-81, Manchester, UK, June 2012. Springer.
[ bib |
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.
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR-7986, INRIA, June 2012.
[ bib |
full paper on HAL |
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
|||Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Built-in treatment of an axiomatic floating-point theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ]|
|||Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ]|
|||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 45-59, Saarbrücken, Germany, April 2011. Springer. [ bib | DOI | .pdf | Abstract ]|
|||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 ]|
|||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 ]|
|||Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation temps-réel de programmes Caml. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ]|
|||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 287-303, Trento, Italy, September 2009. Springer. [ bib | DOI ]|
|||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 1-5, 2008. [ bib | DOI | PDF | .pdf | Abstract ]|
|||Sylvain Conchon, Jean-Christophe 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 8th International Symposium on Trends in Functional Programming (TFP'07), New York, USA, volume 8. Intellect, 2008. [ bib ]|
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
In Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198(2) of
Electronic Notes in Computer Science, pages 51-69. Elsevier Science
[ bib |
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.
Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer.
SAT-MICRO : petit mais costaud !
In Dix-neuvièmes Journées Francophones des Langages
Applicatifs, Étretat, France, January 2008. INRIA.
[ bib |
Le problème SAT, qui consiste `a déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers 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 non-chronologique 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 SAT-solver, baptisé SAT-MICRO, intégrant ces optimisations. Le fonctionnement de SAT-MICRO 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.
|||Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]|
|||François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ]|
|||Sylvain Conchon and Évelyne Contejean. The Alt-Ergo automatic theorem prover. http://alt-ergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000. [ bib | http ]|
|||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 ]|
Sylvain Conchon and Jean-Christophe Filliâtre.
A Persistent Union-Find Data Structure.
In ACM SIGPLAN Workshop on ML, pages 37-45, Freiburg, Germany,
October 2007. ACM.
[ bib |
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.
Sylvain Conchon, Jean-Christophe 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 TR-SHU-CS-2007-04-1,
pages XII/1-13, New York, USA, April 2007. Seton Hall University.
[ bib |
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.
|||Sylvain Conchon, Jean-Christophe 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 ]|
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane
Lightweight Integration of the Ergo Theorem Prover inside a Proof
In John Rushby and N. Shankar, editors, Proceedings of the
second workshop on Automated formal methods, pages 55-59. ACM Press, 2007.
[ bib |
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.
|||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 ]|
Sylvain Conchon and Jean-Christophe Filliâtre.
In Dix-huitièmes Journées Francophones des Langages
Applicatifs, pages 135-149. INRIA, January 2007.
[ bib |
Le problème des classes disjointes, connu sous le nom de union-find, 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.
|||Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ]|
|||Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187-210, 2006. Special Issue of TCS dedicated to a refereed selection of papers presented at TACAS'03. [ bib ]|
|||Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(1-2):87-106, May 2005. [ bib ]|
|||Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 79-94. INRIA, March 2005. [ bib | .ps.gz ]|
|||Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. In Franz Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Computer Science, Miami Beach, FL, USA, July 2003. Springer. [ bib | .ps.gz ]|
|||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 537-553, Warsaw, Poland, April 2003. Springer. [ bib | .ps.gz ]|
|||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 ]|
|||Sylvain Conchon and François Pottier. JOIN(X): Constraint-based type inference for the join-calculus. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in Computer Science, pages 221-236, Genova, Italy, April 2001. Springer. [ bib | .ps.gz ]|
|||François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pages 46-57, Montréal, Canada, September 2000. [ bib | .ps.gz ]|
|||Sylvain Conchon and Fabrice Le Fessant. Jocaml: Mobile agents for Objective-Caml. In First International Symposium on Agent Systems and Applications and Third International Symposium on Mobile Agents (ASA/MA'99), pages 22-29, Palm Springs, California, October 1999. [ bib | .ps.gz ]|
This page was generated by bibtex2html.