Background
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts.
Aims and Scope
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
- Decision procedures and theories of interest
- Combinations of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Applications and case studies
- Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well as novel applications of SMT, are especially encouraged.
Related events
The SMT workshop is traditionally organized in partnership with the
SMT competition.
Check out the SMT-COMP 2012 web page for the results!
Program committee
- Clark Barrett (New York University)
- Nikolaj Bjørner (Microsoft)
- Roberto Bruttomesso (Atrenta)
- Sylvain Conchon (LRI& University of Paris-Sud)
- Bruno Dutertre (SRI)
- Pascal Fontaine (INRIA, University of Nancy), co-chair
- Vijay Ganesh (MIT)
- (Intel), co-chair
- Franjo Ivančić (NEC)
- Sava Krstic (Intel)
- Viktor Kuncak (EPFL)
- Shuvendu Lahiri (Microsoft)
- Ken McMillan (Microsoft)
- Roberto Sebastiani (University of Trento)
- Cesare Tinelli (The University of Iowa )
Paper submission and Proceedings
Three categories of submissions are invited:
- Extended abstracts: given the informal style of the workshop, we strongly encourage the submission of preliminary reports of work in progress. They may range in length from very short (a couple of pages) to the full 10 pages and they will be judged based on the expected level of interest for the SMT community. They will be included in the informal proceedings.
- Original papers: contain original research (simultaneous submissions are not allowed) and sufficient detail to assess the merits and relevance of the submission. For papers reporting experimental results, authors are strongly encouraged to make their data available.
- Presentation-only papers: describe work recently published or submitted and will not be included in the proceedings. We see this as a way to provide additional access to important developments that SMT Workshop attendees may be unaware of.
Papers in all three categories are peer-reviewed.
Important dates:
- Submission deadline: April 16th, 2012 April 24th, 2012
- Notification: May 7th, 2012 May 22th, 2012
- Camera ready versions due: June 1st, 2012
- Workshop: June 30th and July 1st, 2012
Proceedings
Download here the full SMT 2012 pre-proceedings.
Download here the full SMT-COMP 2012 report.
Get here system descriptions for SMT-COMP 2012 participants.
Program (tentative)
All talks will take place at Kilburn Building, Lecture Theatre 1.1.Saturday, 30 June 2012
| 08:55 - 09:00 | Welcome |
| Session 1: | Invited Talk. Chair: Nikolaj Bjørner |
| 09:00 - 10:00 | Natarajan Shankar Invited Talk: The Architecture of Inference from SMT to ETB Abstract: Modularity plays a central role in logical reasoning. We want to be able to reuse proofs, proof patterns, theories, and specialized reasoning procedures. Architectures that support modularity have been developed at all levels of inference: SAT solvers, theory solvers, combination solvers and rewriters, SMT solvers, simplifiers, rewriters, and tactics-based interactive theorem provers. Prior work has mostly focused on fine-grained modular inference. However, with the availability of a diverse range of high-quality inference tools, it has become important to systematically integrate these big components into robust toolchains. At SRI, we have been developing a framework called the Evidential Tool Bus (ETB) as a distributed platform for the coarse-grained integration of inference components into flexible, scriptable workflows. The talk describes the architecture of ETB along with some motivating applications. |
| 10:00 - 10:30 | Coffee break |
| Session 2: | Procedures. Chair: Alberto Griggio |
| 10:30 - 11:00 | Claire Dross, Sylvain Conchon, Johannes Kanig and Andrei Paskevich Reasoning with Triggers |
| 11:00 - 11:30 | Anh-Dung Phan, Nikolaj Bjørner and David Monniaux Anatomy of Alternating Quantifier Satisfiability (Work in progress) |
| 11:30 - 12:00 | Stephan Falke, Carsten Sinz and Florian Merz A Theory of Arrays with set and copy Operations (Extended abstract) |
| 12:00 - 14:00 | Lunch break |
| Session 3: | Arithmetic. Chair: Leonardo de Moura |
| 14:00 - 14:30 | Michael Codish, Yoav Fekete, Carsten Fuhs, Jürgen Giesl and Johannes Waldmann Exotic Semi-Ring Constraints (Extended abstract) |
| 14:30 - 15:00 | Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed Iguernelala Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers |
| 15:00 - 15:30 | Coffee break |
| Session 4: | |
| 15:30 - 18:00 | Business Meeting SMT-COMP (download here the full SMT-COMP 2012 report) SMT-LIB |
| 18:00 - 19.15 | Informal Bar session, joint with PAAR'12 Rain Bar 80 Great Bridgewater, Manchester, M1 5JG |
| 19:30 - | Informal dinner, joint with PAAR'12 EastZEast Riverside Blackfriars Street, Deansgate, Manchester, M3 5BQ The cost of the dinner is 23.95 pounds 30 minutes walk away from conference venue |
the dinner will take place in the EastZEast
Restaurant, Riverside (Blackfriars Street, Deansgate, Manchester,
M3 5BQ) at 19:30 on Saturday, 30 June 2012 (the first day of the
workshop). The cost of the dinner is 23.95 pounds.
You are also invited to drop into the Rain Bar (80 Great
Bridgewater, Manchester, M1 5JG) before going to the dinner on
Saturday.
Sunday, 1 July 2012
| Session 5: | Invited Talk. Joint with PAAR 2012. Chair: Pascal Fontaine |
| 09:00 - 10:00 | Armin Biere Invited Talk: Practical Aspects of SAT Solving Abstract: SAT solving techniques are used in many automated reasoning engines. This talk gives an overview on recent developments in practical aspects of SAT solver development. Beside improvements of the basic conflict driven clause learning (CDCL) algorithm, we also discuss improving and integrating advanced preprocessing techniques as inprocessing during search. The talk concludes with a brief overview on current trends in parallelizing SAT. |
| 10:00 - 10:30 | Coffee break |
| Session 6: | SMT-LIB. Chair: Clark Barrett |
| 10:30 - 11:00 | Nikolaj Bjørner, Vijay Ganesh, Raphaël Michel and Margus Veanes An SMT-LIB Format for Sequences and Regular Expressions (Extended abstract) |
| 11:00 - 11:30 | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina Reachability Modulo Theory Library (Extended abstract) |
| 11:30 - 12:00 | Nikolaj Bjørner, Kenneth McMillan and Andrey Rybalchenko Program Verification as Satisfiability Modulo Theories |
| 12:00 - 13:30 | Lunch break |
| Session 7: | Applications. Chair: Bruno Dutertre |
| 13:30 - 14:00 | Temesghen Kahsai, Yeting Ge and Cesare Tinelli Invariant discovery by efficient sifting (Presentation only) |
| 14:00 - 14:30 | Amit Goel, Sava Krstic, Rebekah Leslie and Mark Tuttle SMT-Based System Verification with DVF |
| 14:30 - 15:00 | Raphaël Michel, Vijay Ganesh, Arnaud Hubaux and Patrick Heymans An SMT-based approach to automated configuration (Extended abstract) |
| 15:00 - 15:30 | Coffee break |
| Session 8: | Bit-vectors. Chair: Amit Goel |
| 15:30 - 16:00 | Gergely Kovásznai, Andreas Fröhlich and Armin Biere On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width |
| 16:00 - 16:30 | Mohammad Abdul Aziz, Amr Wassal and Nevine Darwish A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems (Work in progress) |
Previous editions
More information about the SMT workshop series can be found on The International Workshop on Satisfiability Modulo Theories Website- SMT 2012, Manchester, UK - affiliated with IJCAR 2012
- SMT 2011, Snowbird, USA - affiliated with CAV 2011
- SMT 2010, Edinburgh, UK - affiliated with CAV 2010 and SAT 2010
- SMT 2009, Montreal, Canada - affiliated with CADE-22
- SMT 2008, Princeton, USA - affiliated with CAV 2008
- SMT 2007, Berlin, Germany - affiliated with CAV 2007
- PDPAR 2006, Seattle, USA - affiliated with IJCAR 2006
- PDPAR 2005, Edinburgh, UK - affiliated with CAV 2005
- PDPAR 2004, Cork, Ireland - affiliated with IJCAR 2004
- PDPAR 2003, Miami, USA - affiliated with CADE-19