Sylvain Conchon

According to our database, Sylvain Conchon authored at least 45 papers between 1999 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker.

Sylvain Conchon, Alexandrina Korneva

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

2022

Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk).

Sylvain Conchon

Proceedings of the 5th International Symposium on Foundations and Applications of Blockchain 2022, 2022

2021

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker.

Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando

Fundam. Informaticae, 2021

On the Parameterized Verification of Abstract Models of Contact Tracing Protocols.

Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier

Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, 2021

Verification of Contact Tracing Protocols via SMT-based Model Checking and Counting Abstraction.

Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier

Proceedings of the 36th Italian Conference on Computational Logic, 2021

Formally Documenting Tenderbake (Short Paper).

Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, Alain Mebsout

Proceedings of the 3rd International Workshop on Formal Methods for Blockchains, 2021

2020

Parameterized Model Checking on the TSO Weak Memory Model.

Sylvain Conchon, David Declerck, Fatiha Zaïdi

J. Autom. Reason., 2020

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

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

Reasoning About Universal Cubes in MCMT.

Sylvain Conchon, Mattias Roux

Proceedings of the Formal Methods and Software Engineering, 2019

Verifying Smart Contracts with Cubicle.

Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

2018

A Non-linear Arithmetic Procedure for Control-Command Software Verification.

Pierre Roux, Mohamed Iguernlala, Sylvain Conchon

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols.

Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando

Proceedings of the Networked Systems - 6th International Conference, 2018

Cubicle- <i>W</i> : Parameterized Model Checking on Weak Memory.

Sylvain Conchon, David Declerck, Fatiha Zaïdi

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Parameterized Model Checking Modulo Explicit Weak Memory Models.

Sylvain Conchon, David Declerck, Fatiha Zaïdi

Proceedings of the Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), 2017

Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- <i>W</i>.

Sylvain Conchon, David Declerck, Fatiha Zaïdi

Proceedings of the Formal Methods and Software Engineering, 2017

FAR-Cubicle - A new reachability algorithm for Cubicle.

Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT.

Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers.

Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich

J. Autom. Reason., 2016

AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo.

Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout

Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, 2016

Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo.

Sylvain Conchon, Mohamed Iguernelala

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2016

2015

Certificates for Parameterized Model Checking.

Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi

Proceedings of the FM 2015: Formal Methods, 2015

2014

Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières.

Sylvain Conchon, David Declerck, Luc Maranget, Alain Mebsout

Proceedings of the 25. Journées francophones des langages applicatifs, 2014

Tuning the Alt-Ergo SMT Solver for B Proof Obligations.

Sylvain Conchon, Mohamed Iguernelala

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013

A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo.

Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout

Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

Invariants for finite instances and beyond.

Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala

Log. Methods Comput. Sci., 2012

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper.

Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Reasoning with Triggers.

Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers.

Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

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

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

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

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories.

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

2010

Ground Associative and Commutative Completion Modulo Shostak Theories.

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

2009

Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme.

Stéphane Lescuyer, Sylvain Conchon

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

2008

Semi-persistent Data Structures.

Sylvain Conchon, Jean-Christophe Filliâtre

Proceedings of the Programming Languages and Systems, 2008

2007

CC(X): Semantic Combination of Congruence Closure with Solvable Theories.

Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer

Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Designing a Generic Graph Library Using ML Functors.

Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

A persistent union-find data structure.

Sylvain Conchon, Jean-Christophe Filliâtre

Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007, 2007

2006

Strategies for combining decision procedures.

Sylvain Conchon, Sava Krstic

Theor. Comput. Sci., 2006

Type-safe modular hash-consing.

Jean-Christophe Filliâtre, Sylvain Conchon

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

2005

Canonization for disjoint unions of theories.

Sava Krstic, Sylvain Conchon

Inf. Comput., 2005

2001

JOIN(X): Constraint-Based Type Inference for the Join-Calculus.

Sylvain Conchon, François Pottier

Proceedings of the Programming Languages and Systems, 2001

2000

Information flow inference for free.

François Pottier, Sylvain Conchon

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1999

Jocaml: Mobile Agents for Objective-Caml.

Sylvain Conchon, Fabrice Le Fessant

Proceedings of the 1st International Symposium on Agent Systems and Applications / 3rd International Symposium on Mobile Agents (ASA/MA '99), 1999