default search action
Sylvain Conchon
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [c38]Sylvain Conchon, Alexandrina Korneva:
The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. SEFM 2023: 30-46 - 2022
- [c37]Sylvain Conchon:
Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk). FAB 2022: 2:1-2:1 - 2021
- [j8]Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando:
Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker. Fundam. Informaticae 178(4): 347-378 (2021) - [c36]Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, Alain Mebsout:
Formally Documenting Tenderbake (Short Paper). FMBC@CAV 2021: 4:1-4:9 - [c35]Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier:
Verification of Contact Tracing Protocols via SMT-based Model Checking and Counting Abstraction. CILC 2021: 77-91 - [c34]Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier:
On the Parameterized Verification of Abstract Models of Contact Tracing Protocols. OVERLAY@GandALF 2021: 61-66 - 2020
- [j7]Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Parameterized Model Checking on the TSO Weak Memory Model. J. Autom. Reason. 64(7): 1307-1330 (2020) - [i2]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 abs/2005.07191 (2020)
2010 – 2019
- 2019
- [j6]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): 221-259 (2019) - [c33]Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi:
Verifying Smart Contracts with Cubicle. FM Workshops (1) 2019: 312-324 - [c32]Sylvain Conchon, Mattias Roux:
Reasoning About Universal Cubes in MCMT. ICFEM 2019: 270-285 - 2018
- [c31]Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Cubicle- W : Parameterized Model Checking on Weak Memory. IJCAR 2018: 152-160 - [c30]Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando:
Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols. NETYS 2018: 209-224 - [c29]Pierre Roux, Mohamed Iguernlala, Sylvain Conchon:
A Non-linear Arithmetic Procedure for Control-Command Software Verification. TACAS (2) 2018: 132-151 - [i1]Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux:
FAR-Cubicle - A new reachability algorithm for Cubicle. CoRR abs/1811.08131 (2018) - 2017
- [c28]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: 419-435 - [c27]Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux:
FAR-Cubicle - A new reachability algorithm for Cubicle. FMCAD 2017: 172-175 - [c26]Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- W. ICFEM 2017: 88-104 - [c25]Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Parameterized Model Checking Modulo Explicit Weak Memory Models. IMPEX/FM&MDD 2017: 48-63 - 2016
- [j5]Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich:
Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. J. Autom. Reason. 56(4): 387-457 (2016) - [c24]Sylvain Conchon, Mohamed Iguernelala:
Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo. RSSRail 2016: 243-253 - [c23]Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout:
AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo. UITP 2016: 1-13 - 2015
- [c22]Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi:
Certificates for Parameterized Model Checking. FM 2015: 126-142 - [e1]Michael J. Butler, Sylvain Conchon, Fatiha Zaïdi:
Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings. Lecture Notes in Computer Science 9407, Springer 2015, ISBN 978-3-319-25422-7 [contents] - 2014
- [c21]Sylvain Conchon, Mohamed Iguernelala:
Tuning the Alt-Ergo SMT Solver for B Proof Obligations. ABZ 2014: 294-297 - [c20]Sylvain Conchon, David Declerck, Luc Maranget, Alain Mebsout:
Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. JFLA 2014: 17-32 - 2013
- [c19]Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi:
Invariants for finite instances and beyond. FMCAD 2013: 61-68 - [c18]Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout:
A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. SYNASC 2013: 161-168 - 2012
- [j4]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) - [c17]Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala:
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. SMT@IJCAR 2012: 12-21 - [c16]Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich:
Reasoning with Triggers. SMT@IJCAR 2012: 22-31 - [c15]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: 67-81 - [c14]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: 718-724 - 2011
- [j3]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): 159-185 (2011) - [c13]Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala:
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. TACAS 2011: 45-59 - 2010
- [c12]Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala:
Ground Associative and Commutative Completion Modulo Shostak Theories. LPAR short papers(Yogyakarta) 2010: 35-40
2000 – 2009
- 2009
- [c11]Stéphane Lescuyer, Sylvain Conchon:
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. FroCoS 2009: 287-303 - 2008
- [c10]Sylvain Conchon, Jean-Christophe Filliâtre:
Semi-persistent Data Structures. ESOP 2008: 322-336 - 2007
- [c9]Sylvain Conchon, Jean-Christophe Filliâtre:
A persistent union-find data structure. ML 2007: 37-46 - [c8]Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles:
Designing a Generic Graph Library Using ML Functors. Trends in Functional Programming 2007: 124-140 - [c7]Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer:
CC(X): Semantic Combination of Congruence Closure with Solvable Theories. SMT@CAV 2007: 51-69 - 2006
- [j2]Sylvain Conchon, Sava Krstic:
Strategies for combining decision procedures. Theor. Comput. Sci. 354(2): 187-210 (2006) - [c6]Jean-Christophe Filliâtre, Sylvain Conchon:
Type-safe modular hash-consing. ML 2006: 12-19 - 2005
- [j1]Sava Krstic, Sylvain Conchon:
Canonization for disjoint unions of theories. Inf. Comput. 199(1-2): 87-106 (2005) - 2003
- [c5]Sava Krstic, Sylvain Conchon:
Canonization for Disjoint Unions of Theories. CADE 2003: 197-211 - [c4]Sylvain Conchon, Sava Krstic:
Strategies for Combining Decision Procedures. TACAS 2003: 537-552 - 2001
- [c3]Sylvain Conchon, François Pottier:
JOIN(X): Constraint-Based Type Inference for the Join-Calculus. ESOP 2001: 221-236 - 2000
- [c2]François Pottier, Sylvain Conchon:
Information flow inference for free. ICFP 2000: 46-57
1990 – 1999
- 1999
- [c1]Sylvain Conchon, Fabrice Le Fessant:
Jocaml: Mobile Agents for Objective-Caml. ASA/MA 1999: 22-29
Coauthor Index
aka: Mohamed Iguernelala
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-25 20:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint