SMT Workshop 2012

10th International Workshop on Satisfiability Modulo Theories

Affiliated with the 6th International Joint Conference on Automated Reasoning
(IJCAR 2012)

June 30th, July 1st, 2012

Manchester

See also SMT-COMP 2012


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:

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


Paper submission and Proceedings

Three categories of submissions are invited:

Papers in all three categories are peer-reviewed.

Important dates:

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

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.
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

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

Sponsors

We are grateful to Microsoft and Intel, our sponsors for the 2012 edition of SMT.