conchon.bib

@inproceedings{ConchonIJMF17,
  author = {Sylvain Conchon and
               Mohamed Iguernelala and
               Kailiang Ji and
               Guillaume Melquiond and
               Cl{\'{e}}ment Fumex},
  title = {A Three-Tier Strategy for Reasoning About Floating-Point Numbers in
               {SMT}},
  booktitle = {Computer Aided Verification - 29th International Conference, {CAV}
               2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
  pages = {419--435},
  year = {2017},
  abstract = {  The SMT-LIB standard defines a formal semantics for a theory of
  floating-point (FP) arithmetic (FPA). This formalization reduces FP
  operations to reals by means of a rounding operator, as done
  in the IEEE-754 standard. Closely following this description, we propose
  a three-tier strategy to reason about FPA in SMT solvers. The first
  layer is a purely axiomatic implementation of the automatable
  semantics of the SMT-LIB standard. It reasons with exceptional cases
  (e.g. overflows, division by zero, undefined operations)
  and reduces finite representable FP expressions to reals using the
  rounding operator. At the core of our strategy, a second layer
  handles a set of lemmas about the properties of rounding. For these
  lemmas to be used effectively, we extend the instantiation mechanism
  of SMT solvers to tightly cooperate with the third layer, the NRA
  engine of SMT solvers, which provides interval information.  We
  implemented our strategy in the Alt-Ergo SMT solver and validated
  it on a set of benchmarks coming from the SMT-LIB competition, but
  also from the deductive verification of C and SPARK programs. The
  results show that our approach is promising and compete with
  existing techniques implemented in state-of-the-art SMT solvers.
}
}
@article{DrossCKP16,
  author = {Claire Dross and
               Sylvain Conchon and
               Johannes Kanig and
               Andrei Paskevich},
  title = {Adding Decision Procedures to {SMT} Solvers Using Axioms with Triggers},
  journal = {J. Autom. Reasoning},
  volume = {56},
  number = {4},
  pages = {387--457},
  year = {2016}
}
@inproceedings{ConchonI16,
  author = {Sylvain Conchon and
               Mohamed Iguernelala},
  title = {Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo},
  booktitle = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis,
               Verification, and Certification - First International Conference,
               RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings},
  pages = {243--253},
  year = {2016},
  abstract = {
    In this paper, we report on our recent improvements in the
  Alt-Ergo SMT solver to make it effective in discharging proof
  obligations (POs) translated from the Atelier-B framework. In
  particular, we made important modifications in its internal data
  structures to boost performances of its core decision procedures, we
  improved quantifiers instantiation heuristics, and enhanced the
  interaction between the SAT solver and the decision procedures. We
  also introduced a new plugin architecture to facilitate experiments
  with different SAT engines, and implemented a profiling plugin to
  track and identify ``bottlenecks'' when a formula requires a long
  time to be discharged, or makes the solver
  timeout. Experiments made with more than 10,000 POs
  generated from real industrial B projects show significant
  improvements compared to both previous versions of Alt-Ergod and
  Aterlier-B's automatic main prover.}
}
@inproceedings{ConchonIM17,
  author = {Sylvain Conchon and
               Mohamed Iguernelala and
               Alain Mebsout},
  title = {AltGr-Ergo, a Graphical User Interface for the {SMT} Solver Alt-Ergo},
  booktitle = {Proceedings of the 12th Workshop on User Interfaces for Theorem Provers,
               {UITP} 2016, Coimbra, Portugal, 2nd July 2016.},
  pages = {1--13},
  year = {2016},
  abstract = {   Due to undecidability and complexity of first-order logic, SMT
  solvers may not terminate on some problems or require a very long
  time.  When this happens, one would like to find the reasons why the
  solver fails. To this end, we have designed \agr, an interactive
  graphical interface for the SMT solver AltGr-Ergo which allows users and
  tool developers to help the solver finish some proofs. AltGr-Ergo gives
  real time feedback in order to evaluate and quantify progress made
  by the solver, and also offers various syntactic manipulation
  options to allow a finer grained interaction with AltGr-Ergo. This paper
  describes these features and their implementation, and gives usage
  scenarios for most of them.
}
}
@inproceedings{ConchonMZ15,
  author = {Sylvain Conchon and
               Alain Mebsout and
               Fatiha Za{\"{\i}}di},
  title = {Certificates for Parameterized Model Checking},
  booktitle = {{FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway,
               June 24-26, 2015, Proceedings},
  pages = {126--142},
  year = {2015},
  abstract = {  This paper presents a technique for the certification of Cubicle, a
  model checker for proving safety properties of parameterized
  systems. To increase the confidence in its results, Cubicle now
  produces a proof object (or certificate) that, if proven valid,
  guarantees that the answer for this specific input is correct.
%
  The main challenges addressed in this paper are (1) the production
  of such certificates without degrading the performances of the model
  checker and (2) the construction of these proof objects so that they
  can be independently and efficiently verified by an SMT
  solver. Since the burden of correctness insurance now relies on this
  external solver, a stronger guarantee is obtained by the use of
  multiple backend automatic provers for redundancy.
%
  Experiments show that our approach does not impact Cubicle's
  performances and that we were able to verify certificates for
  challenging parameterized problems. As a byproduct, these
  certificates allowed us to find subtle and critical implementation
  bugs in Cubicle.}
}
@proceedings{icfem2015,
  editor = {Michael Butler and
               Sylvain Conchon and
               Fatiha Za{\"{\i}}di},
  title = {Formal Methods and Software Engineering - 17th International Conference
               on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November
               3-5, 2015, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {9407},
  publisher = {Springer},
  year = {2015},
  isbn = {978-3-319-25422-7}
}
@inproceedings{ConchonI14,
  author = {Sylvain Conchon and
               Mohamed Iguernelala},
  title = {Tuning the Alt-Ergo {SMT} Solver for {B} Proof Obligations},
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
               Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  pages = {294--297},
  year = {2014}
}
@inproceedings{ConchonDMM14,
  author = {Sylvain Conchon and
               David Declerck and
               Luc Maranget and
               Alain Mebsout},
  title = {V{\'{e}}rification de programmes {C} concurrents avec Cubicle
               : Enfoncer les barri{\`{e}}res},
  booktitle = {25. Journ{\'{e}}es francophones des langages applicatifs, Fr{\'{e}}jus,
               France, January 8-11, 2014.},
  pages = {17--32},
  year = {2014}
}
@inproceedings{conchonSMT12,
  author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and
                  Mohamed Iguernelala},
  title = {{Built-in Treatment of an Axiomatic Floating-Point Theory for
                  SMT Solvers}},
  booktitle = {SMT workshop 2012},
  year = {To appear},
  location = {Manchester, UK}
}
@inproceedings{drossSMT12,
  author = {Claire Dross and Sylvain Conchon and Johannes Kanig and
                  Andrei Paskevich},
  title = {{Reasoning with Triggers}},
  booktitle = {SMT workshop 2012},
  year = {To appear},
  location = {Manchester, UK}
}
@article{conchonLMCS12,
  author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
  title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories: Design and Implementation}},
  journal = {Logical Methods in Computer Science},
  year = {To appear}
}
@inproceedings{conchon12cav,
  author = {Sylvain Conchon and Amit Goel and Sava Krsti{\'c}
                  and Alain Mebsout and Fatiha Za\"idi},
  title = {{Cubicle: A Parallel SMT-based Model Checker for
                  Parameterized Systems}},
  booktitle = {CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification},
  year = {2012},
  editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
  series = {Lecture Notes in Computer Science},
  month = {July},
  address = {Berkeley, California, USA},
  publisher = {Springer Verlag},
  abstract = { 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.}
}
@inproceedings{bobot12ijcar,
  author = {Fran\c cois Bobot and Sylvain Conchon and
  Evelyne Contejean and Mohamed Iguernelala and
  Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
  title = {{A Simplex-Based Extension of Fourier-Motzkin for
                  Solving Linear Integer Arithmetic}},
  booktitle = {IJCAR 2012 : Proceedings of the 6th International Joint
                  Conference on Automated Reasoning},
  year = {2012},
  editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
  series = {Lecture Notes in Computer Science},
  address = {Manchester, UK},
  month = {June},
  publisher = {Springer Verlag},
  abstract = {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.}
}
@inproceedings{conchon11tacas,
  author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
  title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
  booktitle = {TACAS 2011: Proceedings of the 17h Tools and Algorithms for the Construction and Analysis of Systems},
  year = 2011,
  month = mar,
  editor = {Parosh A. Abdulla and K. Rustan M. Leino},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  address = {Saarbrucken, Germany},
  url = {http://www.lri.fr/~conchon/publis/conchon-tacas2011.pdf},
  abstract = { AC-completion efficiently handles equality modulo associative and
  commutative function symbols. When the input is ground, the
  procedure terminates and provides a decision algorithm for the word
  problem. In this paper, we present a modular extension of ground
  AC-completion for deciding formulas in the combination of the theory
  of equality with user-defined AC symbols, uninterpreted symbols and
  an arbitrary signature disjoint Shostak theory X.  Our algorithm,
  called AC(X), is obtained by augmenting in a modular way
  ground AC-completion with the canonizer and solver present for the
  theory X. This integration rests on canonized rewriting, a new
  relation reminiscent to normalized rewriting, which integrates
  canonizers in rewriting steps. AC(X) is proved sound, complete
  and terminating, and is implemented to extend the core of the
  Alt-Ergo theorem prover.
  }
}
@inproceedings{conchon10lpar17short,
  author = {Sylvain Conchon and Evelyne Contejean and Mohame Iguernelala},
  title = {Ground Associative and Commutative Completion Modulo Shostak Theories},
  booktitle = {LPAR 17},
  year = {2010},
  address = {Yogyakarta, Indonesia},
  note = {Short paper},
  publisher = {Easychair Proceedings},
  url = {htpp://www.lri.fr/~conchon/publis/conchon-lpar17-short.pdf},
  abstract = {AC-completion efficiently handles equality modulo associative and
  commutative function symbols. In the ground case, the procedure
  terminates and provides a decision algorithm for the word
  problem. In this paper, we present a modular extension of ground
  AC-completion for deciding formulas in the combination of the theory
  of equality with user-defined AC symbols, uninterpreted symbols and
  an arbitrary signature disjoint Shostak theory X. The main ideas
  of our algorithm are first to adapt the definition of rewriting in
  order to integrate the canonizer of X and second, to replace the
  equation orientation mechanism found in ground AC-completion with
  the solver for X.}
}
@inproceedings{conchon10jfla,
  author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe 
 and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
  title = {{Observation temps-r\'e\`el de programmes Caml}},
  year = {2010},
  address = {Vieux-Port La Ciotat, France},
  publisher = {Hermann},
  url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf},
  abstract = {Pour mettre au point un programme, tant du point de vue de sa
  correction que de ses performances, il est naturel de chercher \`a
  observer son ex\'ecution. On peut ainsi cherche \`a observer la gestion
  de la m\'emoire, le temps pass\'e dans une certaine partie du code, ou
  encore certaines valeurs calcul\'ees par le programme.  De nombreux
  outils permettent de telles observations (moniteur syst\`eme,
  profiler ou debugger g\'en\'eriques ou sp\'ecifiques au
  langage, instrumentation explicite du code, etc.).  Ces outils ne
  proposent cependant que des analyses << apr\`es coup >> ou des
  observations tr\`es limit\'ees.  Cet article pr\'esente Ocamlviz une
  biblioth\`eque pour instrumenter du code Ocaml et des outils pour
  visualiser ensuite son ex\'ecution, en temps-r\'eel et de mani\`ere
  distante.}
}
@inproceedings{lescuyer09frocos,
  author = {St{\'e}phane Lescuyer and Sylvain Conchon},
  title = {Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme},
  booktitle = {FroCos},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5749},
  isbn = {978-3-642-04221-8},
  year = {2009},
  pages = {287-303},
  url = {http://www.lri.fr/~conchon/publis/lescuyer-conchon-frocos09.pdf},
  abstract = {In an attempt to improve automation capabilities in the
  Coq proof assistant, we develop a tactic for the propositional
  fragment based on the DPLL procedure. Although formulas naturally
  arising in interactive proofs do not require a state-of-the-art SAT
  solver, the conversion to clausal form required by DPLL strongly
  damages the performance of the procedure. In this paper, we present
  a reflexive DPLL algorithm formalized in Coq which outperforms the
  existing tactics.  It is tightly coupled with a lazy CNF conversion
  scheme which, unlike Tseitin-style approaches, does not disrupt the
  procedure. This conversion relies on a lazy mechanism which requires
  slight adaptations of the original DPLL. As far as we know, this is
  the first formal proof of this mechanism and its Coq implementation
  raises interesting challenges.}
}
@inproceedings{lescuyer08tphol,
  author = {St\'ephane Lescuyer and Sylvain Conchon},
  title = {{A Reflexive Formalization of a SAT Solver in Coq}},
  booktitle = {TPHOLs 2008: In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
  year = 2008,
  url = {http://www.lri.fr/~conchon/publis/lescuyer-conchon-tphols08.pdf},
  abstract = {We present a Coq formalization of an algorithm deciding the 
satisfiability of propositional formulas (SAT). This SAT solver is described 
as a set of inference rules in a manner that is independent of the actual 
representation of propositional variables and formulas. We prove soundness 
and completeness for this system, and instantiate our solver directly on 
the propositional fragment of Coq's logic in order to obtain a fully reflexive
 tactic. Such a tactic represents a first and important step towards our 
ultimate goal of embedding an automated theorem prover inside the Coq system. 
We also extract a certified OCaml implementation of the algorithm}
}
@inproceedings{conchon08smt,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean
  and St\'ephane Lescuyer},
  title = {{Implementing Polymorphism in SMT solvers}},
  booktitle = {SMT '08/BPR '08: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning},
  year = {2008},
  isbn = {978-1-60558-440-9},
  pages = {1--5},
  location = {Princeton, New Jersey},
  doi = {http://doi.acm.org/10.1145/1512464.1512466},
  publisher = {ACM},
  address = {New York, NY, USA},
  url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
  abstract = { Based on our experience with the development of
  Alt-Ergo, we show a small number of modifications needed to bring
  parametric polymorphism to our SMT solver. The first one occurs in
  the typing module where unification is now necessary for solving
  polymorphic constraints over types. The second one consists in
  extending triggers' definition in order to deal with both term and
  type variables. Last, the matching module must be modified to
  account for the instantiation of type variables. We hope that this
  experience is convincing enough to raise interest for polymorphism
  in the SMT community.  }
}
@article{conchon-entcs-08,
  author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
  title = {CC(X): Semantic Combination of Congruence Closure with Solvable Theories},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {198},
  month = {May},
  year = {2008},
  pages = {51-69},
  number = {2},
  url = {http://www.lri.fr/~conchon/publis/conchon-entcs08.pdf},
  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 semantic values for class representatives instead of canonized
terms. Using semantic 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
semantic values.  CC(X) has been implemented in Ocaml and is at
the core of Ergo, a new automated theorem prover dedicated to
program verification.}
}
@inproceedings{ConchonFilliatre08esop,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  booktitle = {17th European Symposium on Programming (ESOP'08)},
  year = 2008,
  address = {Budapest, Hungary},
  note = {Short version of~\cite{ConchonFilliatre07spdsrr}},
  url = {http://www.lri.fr/~conchon/publis/spds-esop08.pdf},
  abstract = {
  A data structure is said to be \emph{persistent} when any update
  operation returns a new structure without altering the old version.
  This paper introduces a new notion of persistence, called
  \emph{semi-persistence}, where only ancestors of the most recent
  version can be accessed or updated. 
  Making a data structure semi-persistent may
  improve its time and space complexity.  This is of particular
  interest in backtracking algorithms manipulating persistent data
  structures, where this property is usually satisfied.
  We propose a proof system to statically check the valid use of
  semi-persistent data structures. It requires a few annotations from
  the user and then generates proof obligations that are
  automatically discharged by a dedicated decision procedure.}
}
@inproceedings{Conchon08,
  author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
  title = {{SAT-Micro : petit mais costaud!}},
  booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2008,
  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 ainsi qu'une mise en forme normale conjonctive
  paresseuse. 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.
}
}
@inproceedings{ConchonAFM07,
  author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Lightweight Integration of the Ergo Theorem Prover inside a
  Proof Assistant}},
  booktitle = {{Second Automated Formal Methods workshop series (AFM07)}},
  year = 2007,
  address = {Atlanta, Georgia, USA},
  month = {November},
  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.
},
  url = {http://www.lri.fr/~conchon/publis/conchon-afm07.pdf}
}
@inproceedings{ConchonFilliatre07,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{A Persistent Union-Find Data Structure}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  year = 2007,
  address = {Freiburg, Germany},
  month = {October},
  abstract = { 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},
  url = {http://www.lri.fr/~conchon/publis/conchon-ml07.ps}
}
@unpublished{Conchon08traces,
  author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig},
  title = {{Lightweight Equality Certificates by Double Blind Traces}},
  url = {http://www.lri.fr/~conchon/publis/traces.ps},
  month = {Oct},
  year = 2007,
  abstract = {We present a mechanism to automate equality proofs in skeptical
  proof assistants. The equality we consider is the combination of the
  pure theory of equality over uninterpreted symbols and a built-in
  decidable theory X. Our approach is intermediate between
  traditional complete proof reconstruction and verified provers.
  Reasoning about X is implemented independently in the proof
  assistant and as an external decision procedure. This double blind
  computation enables both tools to interact only by lightweight
  traces about pure equalities which are produced by the decision
  procedure and interpreted by the proof assistant.
  We validate our approach with the Coq proof assistant and our
  decision procedure CC(X), a congruence closure algorithm modulo a
  built-in theory. CC(X) is implemented as a module parameterized by
  X and the Coq development follows the same modular
  architecture.  Currently, we have instantiated X by the theory of
  linear arithmetic.}
}
@techreport{ConchonFilliatre07spdsrr,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1474},
  month = {September},
  year = 2007,
  url = {http://www.lri.fr/~conchon/publis/spds-rr.pdf},
  abstract = {  
  A data structure is said to be persistent when any update
  operation returns a new structure without altering the old version.
  This paper introduces a new notion of persistence, called
  semi-persistence, where only ancestors of the most recent
  version can be accessed or updated. 
  Making a data structure semi-persistent may
  improve its time and space complexity.  This is of particular
  interest in backtracking algorithms manipulating persistent data
  structures, where this property is usually satisfied.
  We propose a proof system to statically check the valid use of
  semi-persistent data structures. It requires a few annotations from
  the user and then generates proof obligations that are
  automatically discharged by a dedicated decision procedure.
  Additionally, we give some examples of semi-persistent data
  structures (arrays, lists and hash tables).}
}
@inproceedings{conchonsmt07,
  author = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig},
  title = {{CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers}},
  booktitle = {5th International Workshop on Satisfiability Modulo},
  year = 2007,
  address = {Berlin, Germany},
  month = jul,
  topics = {team, lri},
  abstract = {We present a generic congruence closure algorithm for deciding
  ground formulas in the combination of the theory of equality with
  uninterpreted symbols and a union X of solvable theories.  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 approach by the
  use of semantical values for class representatives instead of
  syntactical canonizers.  This seemingly insignificant difference has
  strong impact on efficiency and expressiveness. 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.},
  url = {http://www.lri.fr/~conchon/publis/conchon-smt07.ps}
}
@incollection{conchon07tfpbook,
  author = {Sylvain Conchon and  
     Jean-Christophe Filli\^atre and 
     Julien Signoles},
  title = {{Designing a Generic Graph Library using ML Functors}},
  booktitle = {Trends in Functional Programming},
  publisher = {Intellect},
  year = 2007,
  volume = 8,
  note = {to appear},
  topics = {team, lri},
  type_publi = {irevcomlec}
}
@inproceedings{ocamlgraphTFP07,
  author = {Sylvain Conchon and  
     Jean-Christophe Filli\^atre and 
     Julien Signoles},
  title = {{Designing a Generic Graph Library using ML Functors}},
  booktitle = {The Eighth Symposium on Trends in Functional Programming},
  year = 2007,
  address = {New York, USA},
  month = apr,
  topics = {team, lri},
  type_publi = {icolcomlec},
  abstract = {  
  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.},
  url = {http://www.lri.fr/~conchon/publis/ocamlgraph-tfp07.ps}
}
@inproceedings{ConchonFilliatre06b,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Union-Find Persistant}},
  booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2007,
  address = {Aix-les-bains, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf.ps.gz},
  abstract = {  
  Le probl\`eme des classes disjointes, connu sous le nom de
  union-find, consiste \`a maintenir dans une structure de
  donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
  op\'erations : une fonction find d\'eterminant la classe d'un
  \'el\'ement et une fonction union r\'eunissant deux classes.  Une
  solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
  longtemps.

  Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
  devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
  s'effectuent des retours en arri\`ere (backtracking). Nous
  pr\'esentons dans cet article une version persistante de
  union-find dont la complexit\'e est comparable \`a celle de la
  solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
  utilise massivement des traits imp\'eratifs. C'est pourquoi nous
  pr\'esentons \'egalement une preuve formelle de correction, pour
  s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@inproceedings{ConchonFilliatre06,
  author = {Jean-Christophe Filli\^atre and Sylvain Conchon},
  title = {{Type-Safe Modular Hash-Consing}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  month = {September},
  year = 2006,
  url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz},
  abstract = {  
  Hash-consing is a technique to share values that are structurally
  equal. Beyond the obvious advantage of saving memory blocks,
  hash-consing may also be used to speedup fundamental operations and
  data structures by several orders of magnitude when sharing is
  maximal.  This paper introduces an Ocaml hash-consing library that
  encapsulates hash-consed terms in an abstract datatype, thus safely
  ensuring maximal sharing. This library is also parameterized by an
  equality that allows the user to identify terms according to an
  arbitrary equivalence relation.}
}
@article{conchon-krstic-06,
  author = {Sylvain Conchon and Sava Krsti{\'c}},
  title = {Strategies for combining decision procedures},
  journal = {Theoretical Computer Science},
  volume = {354},
  number = {2},
  year = {2006},
  issn = {0304-3975},
  pages = {187--210},
  doi = {http://dx.doi.org/10.1016/j.tcs.2005.11.025},
  publisher = {Elsevier Science Publishers Ltd.},
  address = {Essex, UK}
}
@inproceedings{ConchonFilliatreSignoles05,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
  title = {Le foncteur sonne toujours deux fois},
  booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = mar,
  year = 2005,
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/ftp/publis/jfla05.ps.gz},
  abstract = {  Cet article pr\'esente Ocamlgraph, une biblioth\`eque g\'en\'erique de graphes pour
  le langage de programmation Ocaml. L'originalit\'e de cette
  biblioth\`eque est de proposer d'une part un grand nombre de
  structures de donn\'ees diff\'erentes pour repr\'esenter les graphes ---
  graphes orient\'es ou non, structures persistantes ou modifi\'ees en
  place, sommets et arcs avec ou sans \'etiquettes, marques sur les
  sommets, etc. --- et d'autre part des algorithmes sur les graphes
  \'ecrits ind\'ependamment de la structure de donn\'ees repr\'esentant les
  graphes. Le codage de ces deux aspects originaux a \'et\'e rendu
  possible par une utilisation massive du syst\`eme de modules d'Ocaml
  et notamment de ses fonctions, les foncteurs.
}
}
@article{krstic-conchon-05,
  author = {Sava Krsti{\'c} and Sylvain Conchon},
  title = {Canonization for disjoint unions of theories},
  journal = {Information and Computation},
  volume = {199},
  month = {May},
  year = {2005},
  pages = {87--106},
  number = {1-2}
}
@inproceedings{krstic-conchon-02,
  author = {Sava Krsti{\'c} and Sylvain Conchon},
  title = {Canonization for Disjoint Unions of Theories},
  booktitle = {Proceedings of the 19th International Conference on Automated Deduction 
                 (CADE-19)},
  editor = {Franz Baader},
  address = {Miami Beach, FL, USA},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2741},
  month = jul,
  year = {2003},
  url = {http://www.lri.fr/~conchon/publis/krstic-conchon.ps.gz},
  abstract = {If there exist efficient procedures (canonizers) for reducing
terms of two first-order theories to canonical form, can one use them
to construct such a procedure for terms of the disjoint union of the
two theories?  We prove this is possible whenever the original
theories are convex. As an application, we prove that algorithms for
solving equations in the two theories (solvers) cannot be
combined in a similar fashion. These results are relevant to the
widely used Shostak's method for combining decision procedures for
theories.  They provide the first rigorous answers to the questions
about the possibility to directly combine canonizers and solvers.}
}
@inproceedings{conchon-krstic-02,
  author = {Sylvain Conchon and Sava Krsti{\'c}},
  title = {Strategies for Combining Decision Procedures},
  booktitle = {Proceedings of the 9th Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03)},
  address = {Warsaw, Poland},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2619},
  pages = {537--553},
  month = apr,
  year = {2003},
  url = {http://www.lri.fr/~conchon/publis/conchon-krstic.ps.gz},
  abstract = { Implementing efficient algorithms for combining decision
  procedures has been a challenge and their correctness precarious. In
  this paper we describe an inference system that has the classical
  Nelson-Oppen procedure at its core and includes several
  optimizations: variable abstraction with sharing, canonization of
  terms at the theory level, and Shostak's streamlined generation of
  new equalities for theories with solvers. 
   The transitions of our system are fine-grained enough to model most
  of the mechanisms currently used in designing combination
  procedures. In particular, with a simple language of regular
  expressions we are able to describe several combination algorithms
  as strategies for our inference system, from the basic Nelson-Oppen
  to the very highly optimized one recently given by Shankar and Ruess.
  Presenting the basic system at a high level of generality and
  non-determinism allows transparent correctness proofs that can be
  extended in a modular fashion whenever a new feature is introduced
  in the system.  Similarly, the correctness proof of any new strategy
  requires only minimal additional proof effort.}
}
@inproceedings{conchon-02,
  author = {Sylvain Conchon},
  title = {Modular Information Flow Analysis for Process Calculi},
  booktitle = {Proceedings of the Foundations of Computer Security Workshop (FCS 2002)},
  editor = {Iliano Cervesato},
  month = jul,
  address = {Copenhagen, Denmark},
  year = {2002},
  url = {http://www.lri.fr/~conchon/publis/conchon-fcs02.ps.gz},
  abstract = {We present a framework to extend, in a modular way, the type systems of process
                  calculi with information-flow annotations that ensure a noninterference property 
                  based on weak barbed bisimulation.  Our method of adding security annotations
                  readily supports modern typing features, such as polymorphism and type
                  reconstruction, together with a noninterference proof. Furthermore,
                  the new systems thus obtained can detect, for instance, information flow caused
                  by contentions on distributed resources, which are not detected in a
                  satisfactory way by using testing equivalences.}
}
@inproceedings{conchon-pottier-01,
  author = {Sylvain Conchon and Fran\c{c}ois Pottier},
  title = {{JOIN(X)}: Constraint-Based Type Inference for the
                 Join-Calculus},
  booktitle = {Proceedings of the 10th European Symposium on
                 Programming (ESOP'01)},
  editor = {David Sands},
  address = {Genova, Italy},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2028},
  pages = {221--236},
  month = apr,
  year = {2001},
  url = {http://www.lri.fr/~conchon/publis/conchon-fpottier-esop01.ps.gz},
  abstract = {We present a generic constraint-based type system for
                 the join-calculus. The key issue is type
                 generalization, which, in the presence of concurrency,
                 must be restricted. We first define a liberal
                 generalization criterion, and prove it correct. Then,
                 we find that it hinders type inference, and propose a
                 cruder one, reminiscent of ML's \emph{value
                 restriction}. We establish type safety using a
                 \emph{semi-syntactic} technique, which we believe is of
                 independent interest. It consists in interpreting
                 typing judgements as (sets of) judgements in an
                 underlying system, which itself is given a syntactic
                 soundness proof. This hybrid approach allows giving
                 pleasant logical meaning to high-level notions such as
                 type variables, constraints and generalization, and
                 clearly separating them from low-level aspects
                 (substitution lemmas, etc.), which are dealt with in a
                 simple, standard way.}
}
@inproceedings{pottier-conchon-icfp-00,
  author = {Fran\c{c}ois Pottier and Sylvain Conchon},
  title = {Information Flow Inference for Free},
  booktitle = {Proceedings of the the Fifth {ACM} {SIGPLAN}
                 International Conference on Functional Programming (ICFP'00)},
  url = {http://www.lri.fr/~conchon/publis/fpottier-conchon-icfp00.ps.gz},
  month = sep,
  year = {2000},
  pages = {46--57},
  address = {Montr\'eal, Canada},
  abstract = {This paper shows how to systematically extend an arbitrary type
                  system with dependency information, and how the new system's
                  soundness and non-interference proofs may rely upon, rather than
                  duplicate, the original system's soundness proof. This allows
                  enriching virtually any of the type systems known today with
                  information flow analysis, while requiring only a minimal proof
                  effort.

                  Our approach is based on an untyped operational semantics for a
                  labelled calculus akin to core ML. Thus, it is simple, and
                  should be applicable to other computing paradigms, such as
                  object or process calculi.

                  The paper also discusses access control, and shows it may be
                  viewed as entirely independent of information flow
                  control. Letting the two mechanisms coexist, without
                  interacting, yields a simple and expressive type system, which
                  allows, in particular, ``selective'' declassification.}
}
@inproceedings{conchon-le-fessant-99,
  title = {Jocaml: Mobile Agents for {Objective-Caml}},
  author = {Sylvain Conchon and Fabrice Le Fessant},
  booktitle = {First International Symposium on Agent Systems and
                 Applications and Third International Symposium on
                 Mobile Agents (ASA/MA'99)},
  address = {Palm Springs, California},
  year = {1999},
  month = oct,
  pages = {22--29},
  url = {http://www.lri.fr/~conchon/publis/conchon-lefessant-asama99.ps.gz},
  abstract = {Jocaml is a system for mobile agents built inside the
                  Objective-Caml language. Jocaml eases the development of concurrent,
                  distributed and mobile agent based applications, by expressing useful
                  distribution abstractions using a small set of simple but powerful primitives
                  taken from the Join-Calculus\cite{FG96}.

                  The system provides total transparency for migration, application states
                  (after migration, all threads resume their execution in the state before
                  migration), communications (communication channels with other agents are kept
                  during migration) and composition (sub-agents migrate with their parent
                  agent). Other features of the Jocaml system are mobile objects with
                  transparent remote method invocation, distributed garbage collection,
                  failure detection and execution efficiency. Jocaml has already been used in
                  several applications, such as a mobile editor, some distributed games and a
                  distributed implementation of Ambients\cite{CG98}.

                  This paper describes the Jocaml programming model and language, its current 
                  implementation and some interesting applications.}
}
@inproceedings{conchon-lan-electre-99,
  title = {Synchrone/Asynchrone: une vue d'Electre},
  author = {Sylvain Conchon},
  booktitle = {Rapport de recherche 99.04},
  address = {IRCyN},
  year = {1999},
  month = feb,
  pages = {28 pages}
}
@inproceedings{conchon-lan-coalgebre-99,
  title = {Alg\`ebres et Coalg\`ebres},
  author = {Sylvain Conchon},
  booktitle = {Rapport de recherche 99.05},
  address = {IRCyN},
  year = {1999},
  month = feb,
  pages = {18 pages}
}

This file was generated by bibtex2html 1.98.