Sylvain Conchon

49 papers A* 1A 8B 4C 4Misc 1Journal 10Unranked 21

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