[1] 
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, and
Clément Fumex.
A threetier strategy for reasoning about floatingpoint numbers in
SMT.
In Computer Aided Verification  29th International Conference,
CAV 2017, Heidelberg, Germany, July 2428, 2017, Proceedings, Part II,
pages 419435, 2017.
[ bib ]
The SMTLIB standard defines a formal semantics for a theory of floatingpoint (FP) arithmetic (FPA). This formalization reduces FP operations to reals by means of a rounding operator, as done in the IEEE754 standard. Closely following this description, we propose a threetier strategy to reason about FPA in SMT solvers. The first layer is a purely axiomatic implementation of the automatable semantics of the SMTLIB 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 AltErgo SMT solver and validated it on a set of benchmarks coming from the SMTLIB 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 stateoftheart SMT solvers.

[2]  Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Adding decision procedures to SMT solvers using axioms with triggers. J. Autom. Reasoning, 56(4):387457, 2016. [ bib ] 
[3] 
Sylvain Conchon and Mohamed Iguernelala.
Increasing proofs automation rate of atelierb thanks to altergo.
In Reliability, Safety, and Security of Railway Systems.
Modelling, Analysis, Verification, and Certification  First International
Conference, RSSRail 2016, Paris, France, June 2830, 2016, Proceedings,
pages 243253, 2016.
[ bib ]
In this paper, we report on our recent improvements in the AltErgo SMT solver to make it effective in discharging proof obligations (POs) translated from the AtelierB 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 AltErgod and AterlierB's automatic main prover.

[4] 
Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout.
Altgrergo, a graphical user interface for the SMT solver altergo.
In Proceedings of the 12th Workshop on User Interfaces for
Theorem Provers, UITP 2016, Coimbra, Portugal, 2nd July 2016., pages
113, 2016.
[ bib ]
Due to undecidability and complexity of firstorder 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 , an interactive graphical interface for the SMT solver AltGrErgo which allows users and tool developers to help the solver finish some proofs. AltGrErgo 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 AltGrErgo. This paper describes these features and their implementation, and gives usage scenarios for most of them.

[5] 
Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi.
Certificates for parameterized model checking.
In FM 2015: Formal Methods  20th International Symposium,
Oslo, Norway, June 2426, 2015, Proceedings, pages 126142, 2015.
[ bib ]
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.

[6]  Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors. Formal Methods and Software Engineering  17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 35, 2015, Proceedings, volume 9407 of Lecture Notes in Computer Science. Springer, 2015. [ bib ] 
[7]  Sylvain Conchon and Mohamed Iguernelala. Tuning the altergo SMT solver for B proof obligations. In Abstract State Machines, Alloy, B, TLA, VDM, and Z  4th International Conference, ABZ 2014, Toulouse, France, June 26, 2014. Proceedings, pages 294297, 2014. [ bib ] 
[8]  Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec cubicle : Enfoncer les barrières. In 25. Journées francophones des langages applicatifs, Fréjus, France, January 811, 2014., pages 1732, 2014. [ bib ] 
[9]  Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Builtin Treatment of an Axiomatic FloatingPoint Theory for SMT Solvers. In SMT workshop 2012, To appear. [ bib ] 
[10]  Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with Triggers. In SMT workshop 2012, To appear. [ bib ] 
[11]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories: Design and Implementation. Logical Methods in Computer Science, To appear. [ bib ] 
[12] 
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, Lecture Notes in Computer Science, Berkeley, California, USA,
July 2012. Springer Verlag.
[ 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 stateoftheart model checkers.

[13] 
François Bobot, Sylvain Conchon, Evelyne 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, Lecture Notes in Computer Science, Manchester, UK, June
2012. Springer Verlag.
[ bib ]
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.

[14] 
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, TACAS
2011: Proceedings of the 17h Tools and Algorithms for the Construction and
Analysis of Systems, Lecture Notes in Computer Science, Saarbrucken,
Germany, March 2011. Springer Verlag.
[ bib 
.pdf ]
ACcompletion 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 ACcompletion for deciding formulas in the combination of the theory of equality with userdefined 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 ACcompletion 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 AltErgo theorem prover.

[15] 
Sylvain Conchon, Evelyne Contejean, and Mohame Iguernelala.
Ground associative and commutative completion modulo shostak
theories.
In LPAR 17, Yogyakarta, Indonesia, 2010. Easychair Proceedings.
Short paper.
[ bib 
.pdf ]
ACcompletion 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 ACcompletion for deciding formulas in the combination of the theory of equality with userdefined 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 ACcompletion with the solver for X.

[16] 
Sylvain Conchon, JeanChristophe Filliâtre, Fabrice Le Fessant, Julien
Robert, and Guillaume Von Tokarski.
Observation tempsréèl de programmes Caml.
VieuxPort La Ciotat, France, 2010. Hermann.
[ bib 
.pdf ]
Pour mettre au point un programme, tant du point de vue de sa correction que de ses performances, il est naturel de chercher à observer son exécution. On peut ainsi cherche à observer la gestion de la mémoire, le temps passé dans une certaine partie du code, ou encore certaines valeurs calculées par le programme. De nombreux outils permettent de telles observations (moniteur système, profiler ou debugger génériques ou spécifiques au langage, instrumentation explicite du code, etc.). Ces outils ne proposent cependant que des analyses << après coup >> ou des observations très limitées. Cet article présente Ocamlviz une bibliothèque pour instrumenter du code Ocaml et des outils pour visualiser ensuite son exécution, en tempsréel et de manière distante.

[17] 
Stéphane Lescuyer and Sylvain Conchon.
Improving coq propositional reasoning using a lazy cnf conversion
scheme.
In FroCos, volume 5749 of Lecture Notes in Computer
Science, pages 287303. Springer, 2009.
[ bib 
.pdf ]
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 stateoftheart 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 Tseitinstyle 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.

[18] 
Stéphane Lescuyer and Sylvain Conchon.
A Reflexive Formalization of a SAT Solver in Coq.
In TPHOLs 2008: In Emerging Trends of the 21st International
Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2008.
[ bib 
.pdf ]
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

[19] 
François Bobot, Sylvain Conchon, Evelyne Contejean, and Stéphane
Lescuyer.
Implementing Polymorphism in SMT solvers.
In SMT '08/BPR '08: Proceedings of the Joint Workshops of the
6th International Workshop on Satisfiability Modulo Theories and 1st
International Workshop on BitPrecise Reasoning, pages 15, New York, NY,
USA, 2008. ACM.
[ bib 
DOI 
.pdf ]
Based on our experience with the development of AltErgo, 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.

[20] 
Sylvain Conchon, Evelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
Cc(x): Semantic combination of congruence closure with solvable
theories.
Electronic Notes in Theoretical Computer Science,
198(2):5169, May 2008.
[ bib 
.pdf ]
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 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.

[21] 
Sylvain Conchon and JeanChristophe Filliâtre.
SemiPersistent Data Structures.
In 17th European Symposium on Programming (ESOP'08), Budapest,
Hungary, 2008.
Short version of [26].
[ bib 
.pdf ]
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 semipersistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semipersistent 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 semipersistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure.

[22] 
Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer.
SATMicro : petit mais costaud!
In Dixneuvièmes Journées Francophones des Langages
Applicatifs, Étretat, France, 2008. INRIA.
[ bib 
.ps ]
Le problème SAT, qui consiste à 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 ainsi qu'une mise en forme normale conjonctive paresseuse. 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.

[23] 
Sylvain Conchon, Evelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
Lightweight Integration of the Ergo Theorem Prover inside a Proof
Assistant.
In Second Automated Formal Methods workshop series (AFM07),
Atlanta, Georgia, USA, November 2007.
[ bib 
.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.

[24] 
Sylvain Conchon and JeanChristophe Filliâtre.
A Persistent UnionFind Data Structure.
In ACM SIGPLAN Workshop on ML, Freiburg, Germany, October 2007.
[ bib 
.ps ]
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

[25] 
Sylvain Conchon, Evelyne Contejean, and Johannes Kanig.
Lightweight Equality Certificates by Double Blind Traces.
Oct 2007.
[ bib 
.ps ]
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 builtin 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 builtin 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.

[26] 
Sylvain Conchon and JeanChristophe Filliâtre.
SemiPersistent Data Structures.
Research Report 1474, LRI, Université Paris Sud, September
2007.
[ bib 
.pdf ]
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 semipersistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semipersistent 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 semipersistent 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 semipersistent data structures (arrays, lists and hash tables).

[27] 
Sylvain Conchon, Evelyne Contejean, and Johannes Kanig.
CC(X): Efficiently Combining Equality and Solvable Theories without
Canonizers.
In 5th International Workshop on Satisfiability Modulo, Berlin,
Germany, July 2007.
[ bib 
.ps ]
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 unionfind datastructure 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.

[28]  Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Trends in Functional Programming, volume 8. Intellect, 2007. to appear. [ bib ] 
[29] 
Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles.
Designing a Generic Graph Library using ML Functors.
In The Eighth Symposium on Trends in Functional Programming,
New York, USA, April 2007.
[ 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.

[30] 
Sylvain Conchon and JeanChristophe Filliâtre.
UnionFind Persistant.
In Dixhuitièmes Journées Francophones des Langages
Applicatifs, Aixlesbains, France, 2007. INRIA.
[ bib 
.ps.gz ]
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.

[31] 
JeanChristophe Filliâtre and Sylvain Conchon.
TypeSafe Modular HashConsing.
In ACM SIGPLAN Workshop on ML, Portland, Oregon, September
2006.
[ bib 
.ps.gz ]
Hashconsing is a technique to share values that are structurally equal. Beyond the obvious advantage of saving memory blocks, hashconsing 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 hashconsing library that encapsulates hashconsed 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.

[32]  Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187210, 2006. [ bib  DOI ] 
[33] 
Sylvain Conchon, JeanChristophe Filliâtre, and Julien Signoles.
Le foncteur sonne toujours deux fois.
In Seizièmes Journées Francophones des Langages
Applicatifs. INRIA, March 2005.
[ bib 
.ps.gz ]
Cet article présente Ocamlgraph, une bibliothèque générique de graphes pour le langage de programmation Ocaml. L'originalité de cette bibliothèque est de proposer d'une part un grand nombre de structures de données différentes pour représenter les graphes  graphes orientés ou non, structures persistantes ou modifiées en place, sommets et arcs avec ou sans étiquettes, marques sur les sommets, etc.  et d'autre part des algorithmes sur les graphes écrits indépendamment de la structure de données représentant les graphes. Le codage de ces deux aspects originaux a été rendu possible par une utilisation massive du système de modules d'Ocaml et notamment de ses fonctions, les foncteurs.

[34]  Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(12):87106, May 2005. [ bib ] 
[35] 
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 Verlag.
[ bib 
.ps.gz ]
If there exist efficient procedures (canonizers) for reducing terms of two firstorder 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.

[36] 
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 Verlag.
[ bib 
.ps.gz ]
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 NelsonOppen 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 finegrained 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 NelsonOppen to the very highly optimized one recently given by Shankar and Ruess. Presenting the basic system at a high level of generality and nondeterminism 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.

[37] 
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 ]
We present a framework to extend, in a modular way, the type systems of process calculi with informationflow 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.

[38] 
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
Verlag.
[ bib 
.ps.gz ]
We present a generic constraintbased type system for the joincalculus. 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 value restriction. We establish type safety using a semisyntactic 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 highlevel notions such as type variables, constraints and generalization, and clearly separating them from lowlevel aspects (substitution lemmas, etc.), which are dealt with in a simple, standard way.

[39] 
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 4657, Montréal,
Canada, September 2000.
[ bib 
.ps.gz ]
This paper shows how to systematically extend an arbitrary type system with dependency information, and how the new system's soundness and noninterference 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.

[40] 
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 ]
Jocaml is a system for mobile agents built inside the ObjectiveCaml 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 JoinCalculus[?].

[41]  Sylvain Conchon. Synchrone/asynchrone: une vue d'electre. In Rapport de recherche 99.04, page 28 pages, IRCyN, February 1999. [ bib ] 
[42]  Sylvain Conchon. Algèbres et coalgèbres. In Rapport de recherche 99.05, page 18 pages, IRCyN, February 1999. [ bib ] 
This file was generated by bibtex2html 1.98.