Jocaml: Mobile Agents for Objective-Caml. - Sylvain Conchon; Fabrice Le Fessant (ASA/MA, 1999)

Information flow inference for free. - François Pottier; Sylvain Conchon (ICFP, 2000)

JOIN(X): Constraint-Based Type Inference for the Join-Calculus. - Sylvain Conchon; François Pottier (ESOP, 2001)

Canonization for disjoint unions of theories. - Sava Krstic; Sylvain Conchon (Inf. Comput., 2005)

Type-safe modular hash-consing. - Jean-Christophe Filliâtre; Sylvain Conchon (ML, 2006)

Strategies for combining decision procedures. - Sylvain Conchon; Sava Krstic (Theor. Comput. Sci., 2006)

A persistent union-find data structure. - Sylvain Conchon; Jean-Christophe Filliâtre (ML, 2007)

Designing a Generic Graph Library Using ML Functors. - Sylvain Conchon; Jean-Christophe Filliâtre; Julien Signoles (Trends in Functional Programming, 2007)

CC(X): Semantic Combination of Congruence Closure with Solvable Theories. - Sylvain Conchon; Evelyne Contejean; Johannes Kanig; Stéphane Lescuyer (SMT@CAV, 2007)

Semi-persistent Data Structures. - Sylvain Conchon; Jean-Christophe Filliâtre (ESOP, 2008)

Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. - Stéphane Lescuyer; Sylvain Conchon (FroCoS, 2009)

Ground Associative and Commutative Completion Modulo Shostak Theories. - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (LPAR short papers(Yogyakarta), 2010)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (TACAS, 2011)

Real-Time Monitoring of Ocaml programs. - Sylvain Conchon; Jean-Christophe Filliâtre; Fabrice Le Fessant; Julien Robert; Guillaume Von Tokarski (Stud. Inform. Univ., 2011)

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. - François Bobot; Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala; Assia Mahboubi; Alain Mebsout; Guillaume Melquiond (IJCAR, 2012)

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. - Sylvain Conchon; Guillaume Melquiond; Cody Roux; Mohamed Iguernelala (SMT@IJCAR, 2012)

Reasoning with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (SMT@IJCAR, 2012)

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. - Sylvain Conchon; Amit Goel; Sava Krstic; Alain Mebsout; Fatiha Zaïdi (CAV, 2012)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (Log. Methods Comput. Sci., 2012)

Invariants for finite instances and beyond. - Sylvain Conchon; Amit Goel; Sava Krstic; Alain Mebsout; Fatiha Zaïdi (FMCAD, 2013)

A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. - Sylvain Conchon; Mohamed Iguernelala; Alain Mebsout (SYNASC, 2013)

Tuning the Alt-Ergo SMT Solver for B Proof Obligations. - Sylvain Conchon; Mohamed Iguernelala (ABZ, 2014)

Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. - Sylvain Conchon; David Declerck; Luc Maranget; Alain Mebsout (JFLA, 2014)

Certificates for Parameterized Model Checking. - Sylvain Conchon; Alain Mebsout; Fatiha Zaïdi (FM, 2015)

Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo. - Sylvain Conchon; Mohamed Iguernelala (RSSRail, 2016)

AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo. - Sylvain Conchon; Mohamed Iguernelala; Alain Mebsout (UITP, 2016)

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (J. Autom. Reason., 2016)

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. - Sylvain Conchon; Mohamed Iguernelala; Kailiang Ji; Guillaume Melquiond; Clément Fumex (CAV (2), 2017)

FAR-Cubicle - A new reachability algorithm for Cubicle. - Sylvain Conchon; Amit Goel; Sava Krstic; Rupak Majumdar; Mattias Roux (FMCAD, 2017)

Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- W. - Sylvain Conchon; David Declerck; Fatiha Zaïdi (ICFEM, 2017)

Parameterized Model Checking Modulo Explicit Weak Memory Models. - Sylvain Conchon; David Declerck; Fatiha Zaïdi (IMPEX/FM&MDD, 2017)

Cubicle- W : Parameterized Model Checking on Weak Memory. - Sylvain Conchon; David Declerck; Fatiha Zaïdi (IJCAR, 2018)

Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols. - Sylvain Conchon; Giorgio Delzanno; Angelo Ferrando 001 (NETYS, 2018)

A Non-linear Arithmetic Procedure for Control-Command Software Verification. - Pierre Roux 001; Mohamed Iguernlala; Sylvain Conchon (TACAS (2), 2018)

Verifying Smart Contracts with Cubicle. - Sylvain Conchon; Alexandrina Korneva; Fatiha Zaïdi (FM Workshops (1), 2019)

Reasoning About Universal Cubes in MCMT. - Sylvain Conchon; Mattias Roux (ICFEM, 2019)

The SMT Competition 2015-2018. - Tjark Weber; Sylvain Conchon; David Déharbe; Matthias Heizmann; Aina Niemetz; Giles Reger (J. Satisf. Boolean Model. Comput., 2019)

Low Cost High Integrity Platform. - Thierry Lecomte; David Déharbe; Denis Sabatier; Étienne Prun; Patrick Péronne; Emmanuel Chailloux; Steven Varoumas; Adilla Susungi; Sylvain Conchon (CoRR, 2020)

Parameterized Model Checking on the TSO Weak Memory Model. - Sylvain Conchon; David Declerck; Fatiha Zaïdi (J. Autom. Reason., 2020)

Formally Documenting Tenderbake (Short Paper). - Sylvain Conchon; Alexandrina Korneva; Çagdas Bozman; Mohamed Iguernlala; Alain Mebsout (FMBC@CAV, 2021)

Verification of Contact Tracing Protocols via SMT-based Model Checking and Counting Abstraction. - Sylvain Conchon; Giorgio Delzanno; Arnaud Sangnier (CILC, 2021)

On the Parameterized Verification of Abstract Models of Contact Tracing Protocols. - Sylvain Conchon; Giorgio Delzanno; Arnaud Sangnier (OVERLAY@GandALF, 2021)

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker. - Sylvain Conchon; Giorgio Delzanno; Angelo Ferrando 001 (Fundam. Informaticae, 2021)

Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk). - Sylvain Conchon (FAB, 2022)

The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. - Sylvain Conchon; Alexandrina Korneva (SEFM, 2023)