| 2023 | SEFM | The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. | Sylvain Conchon, Alexandrina Korneva |
| 2021 | CAV | Formally Documenting Tenderbake (Short Paper). | Sylvain Conchon, Alexandrina Korneva, agdas Bozman, Mohamed Iguernlala, Alain Mebsout |
| 2019 | FM | Verifying Smart Contracts with Cubicle. | Sylvain Conchon, Alexandrina Korneva, Fatiha Zadi |
| 2019 | ICFEM | Reasoning About Universal Cubes in MCMT. | Sylvain Conchon, Mattias Roux |
| 2018 | CADE | Cubicle- | Sylvain Conchon, David Declerck, Fatiha Zadi |
| 2018 | TACAS | A Non-linear Arithmetic Procedure for Control-Command Software Verification. | Pierre Roux, Mohamed Iguernlala, Sylvain Conchon |
| 2017 | CAV | A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. | Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clment Fumex |
| 2017 | FMCAD | FAR-Cubicle - A new reachability algorithm for Cubicle. | Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux |
| 2017 | ICFEM | Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- | Sylvain Conchon, David Declerck, Fatiha Zadi |
| 2015 | FM | Certificates for Parameterized Model Checking. | Sylvain Conchon, Alain Mebsout, Fatiha Zadi |
| 2013 | FMCAD | Invariants for finite instances and beyond. | Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zadi |
| 2013 | SYNASC | A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. | Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout |
| 2012 | CADE | A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. | Franois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
| 2012 | CADE | Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. | Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala |
| 2012 | CADE | Reasoning with Triggers. | Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich |
| 2012 | CAV | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. | Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zadi |
| 2011 | TACAS | Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. | Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala |
| 2010 | LPAR | Ground Associative and Commutative Completion Modulo Shostak Theories. | Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala |
| 2008 | ESOP | Semi-persistent Data Structures. | Sylvain Conchon, Jean-Christophe Fillitre |
| 2003 | CADE | Canonization for Disjoint Unions of Theories. | Sava Krstic, Sylvain Conchon |
| 2003 | TACAS | Strategies for Combining Decision Procedures. | Sylvain Conchon, Sava Krstic |
| 2001 | ESOP | JOIN(X): Constraint-Based Type Inference for the Join-Calculus. | Sylvain Conchon, Franois Pottier |
| 2000 | ICFP | Information flow inference for free. | Franois Pottier, Sylvain Conchon |