Sylvain Conchon

Publication Activity (10 Years)

Years Active: 1999-2023
Publications (10 Years): 23

Top Topics

Temporal Properties

Integer Arithmetic

Top Venues

J. Autom. Reason.

Publications

Sylvain Conchon, Alexandrina Korneva
The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. SEFM (2023)
Sylvain Conchon
Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk). FAB (2022)
Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier
Verification of Contact Tracing Protocols via SMT-based Model Checking and Counting Abstraction. CILC (2021)
Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier
On the Parameterized Verification of Abstract Models of Contact Tracing Protocols. OVERLAY@GandALF (2021)
Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando
Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker. Fundam. Informaticae 178 (4) (2021)
Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, Alain Mebsout
Formally Documenting Tenderbake (Short Paper). FMBC@CAV (2021)
Thierry Lecomte, David Déharbe, Denis Sabatier, Étienne Prun, Patrick Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, Sylvain Conchon
Low Cost High Integrity Platform. CoRR (2020)
Sylvain Conchon, David Declerck, Fatiha Zaïdi
Parameterized Model Checking on the TSO Weak Memory Model. J. Autom. Reason. 64 (7) (2020)
Sylvain Conchon, Mattias Roux
Reasoning About Universal Cubes in MCMT. ICFEM (2019)
Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi
Verifying Smart Contracts with Cubicle. FM Workshops (1) (2019)
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando
Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols. NETYS (2018)
Pierre Roux, Mohamed Iguernlala, Sylvain Conchon
A Non-linear Arithmetic Procedure for Control-Command Software Verification. TACAS (2) (2018)
Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux
FAR-Cubicle - A new reachability algorithm for Cubicle. CoRR (2018)
Sylvain Conchon, David Declerck, Fatiha Zaïdi
: Parameterized Model Checking on Weak Memory. IJCAR (2018)
Sylvain Conchon, David Declerck, Fatiha Zaïdi
Parameterized Model Checking Modulo Explicit Weak Memory Models. IMPEX/FM&MDD (2017)
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. CAV (2) (2017)
Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux
FAR-Cubicle - A new reachability algorithm for Cubicle. FMCAD (2017)
Sylvain Conchon, David Declerck, Fatiha Zaïdi
. ICFEM (2017)
Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout
AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo. UITP (2016)
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. J. Autom. Reason. 56 (4) (2016)
Sylvain Conchon, Mohamed Iguernelala
Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo. RSSRail (2016)
Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi
Certificates for Parameterized Model Checking. FM (2015)
Sylvain Conchon, David Declerck, Luc Maranget, Alain Mebsout
Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. JFLA (2014)
Sylvain Conchon, Mohamed Iguernelala
Tuning the Alt-Ergo SMT Solver for B Proof Obligations. ABZ (2014)
Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout
A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. SYNASC (2013)
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi
Invariants for finite instances and beyond. FMCAD (2013)
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation Log. Methods Comput. Sci. 8 (3) (2012)
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
Reasoning with Triggers. SMT@IJCAR (2012)
Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. SMT@IJCAR (2012)
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. CAV (2012)
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR (2012)
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. TACAS (2011)
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume Von Tokarski
Real-Time Monitoring of Ocaml programs. Stud. Inform. Univ. 9 (1) (2011)
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
Ground Associative and Commutative Completion Modulo Shostak Theories. LPAR short papers(Yogyakarta) (2010)
Stéphane Lescuyer, Sylvain Conchon
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. FroCoS (2009)
Sylvain Conchon, Jean-Christophe Filliâtre
Semi-persistent Data Structures. ESOP (2008)
Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer
CC(X): Semantic Combination of Congruence Closure with Solvable Theories. Electron. Notes Theor. Comput. Sci. 198 (2) (2008)
Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles
Designing a Generic Graph Library Using ML Functors. Trends in Functional Programming (2007)
Sylvain Conchon, Jean-Christophe Filliâtre
A persistent union-find data structure. ML (2007)
Jean-Christophe Filliâtre, Sylvain Conchon
Type-safe modular hash-consing. ML (2006)
Sylvain Conchon, Sava Krstic
Strategies for combining decision procedures. Theor. Comput. Sci. 354 (2) (2006)
Sava Krstic, Sylvain Conchon
Canonization for disjoint unions of theories. Inf. Comput. 199 (1-2) (2005)
Sylvain Conchon, Sava Krstic
Strategies for Combining Decision Procedures. TACAS (2003)
Sava Krstic, Sylvain Conchon
Canonization for Disjoint Unions of Theories. CADE (2003)
Sylvain Conchon, François Pottier
JOIN(X): Constraint-Based Type Inference for the Join-Calculus. ESOP (2001)
François Pottier, Sylvain Conchon
Information flow inference for free. ICFP (2000)
Sylvain Conchon, Fabrice Le Fessant
Jocaml: Mobile Agents for Objective-Caml. ASA/MA (1999)