SMT Workshop 2014

12th International Workshop on Satisfiability Modulo Theories

Affiliated with CAV, IJCAR, and SAT at FLoC 2014

July 17-18, 2014

Vienna, Austria


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 goal of the SMT Workshop is to bring together both researchers and users of SMT technology and provide them with a forum for presenting and discussing both new theoretical ideas and implementation and evaluation techniques. Topics of the workshop 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.

In addition to contributed papers and presentations, the programme of the workshop will include invited presentations, and discussions around the SMT-LIB language, the SMT-EVAL solver evaluation, and the SMT competition, among others.

Invited Speakers

Abstracts of the invited talks.

Programme committee

Tentative Programme

1st Day (July 17th)

09.00 Welcome
09.15 - 10.15 Invited Talk 1: Clark Barrett (New York University)
SMT: Where do we go from here?
Coffee break
Session 1: Applications, reasoning about sets
10:45 - 11.15 Daniel J. Fremont and Sanjit A. Seshia
Speeding Up SMT-Based Quantitative Program Analysis
11:15 - 11.45 Hristina Palikareva and Cristian Cadar
Multi-solver Support in Symbolic Execution (Slides)
11.45 - 12.15 Mats Carlsson, Olga Grinchtein and Justin Pearson
Protocol Log Analysis with Constraint Programming (Slides)
12.15 - 12.45 Edmund S. L. Lam and Iliano Cervesato
Reasoning About Set Comprehensions (Slides)
Lunch break
Session 2: Arrays and polymorphism
14.30 - 15.00 Juergen Christ and Jochen Hoenicke
Weakly Equivalent Arrays (Slides)
15.00 - 15.30 Francesco Alberti, Silvio Ghilardi and Natasha Sharygina
Decision Procedures for Flat Array Properties (Slides)
15.30 - 16.00 Richard Bonichon, David Déharbe and Cláudia Tavares
Extending SMT-LIB v2 with Lambda-Terms and Polymorphism (cancelled)

2nd Day (July 18th)

09.15 - 10.15 Invited Talk 2: Guillaume Melquiond (Inria)
Automating the Verification of Floating-Point Algorithms
Coffee break
Session 3: Arithmetic
10.45 - 11.15 Tim King, Clark Barrett and Cesare Tinelli
Leveraging Linear and Mixed Integer Programming for SMT (Slides)
11.15 - 11.45 To Van Khanh, Vu Xuan Tung and Mizuhito Ogawa
raSAT: SMT for Polynomial Inequality (Slides)
11.45 - 12.15 Marek Kosta, Thomas Sturm and Andreas Dolzmann
Better Answers to Real Questions (Slides)
12.15 - 12.45 Konstantin Korovin, Marek Kosta and Thomas Sturm
Towards Conflict-Driven Learning for Virtual Substitution (Slides)
Lunch break
14.30 - 16.00 SMT-COMP, SMT-EVAL (Slides)
Coffee break
16:30 Business Meeting, SMT-LIB Discussion

Paper submission and Proceedings

Informal proceedings of the workshop appeared in CEUR.

Three categories of submissions are invited:

Papers in all three categories are peer-reviewed.

Original papers should not exceed 10 pages, should be prepared in LaTeX using the easychair.cls class file, and submitted in standard-conforming PDF. Technical details may be included in an appendix to be read at the reviewers' discretion.

To submit a paper, go to the EasyChair SMT page and follow the instructions there.

Important dates

All dates are “anywhere on earth”.

Related events

Previous editions

More information about the SMT workshop series can be found on The International Workshop on Satisfiability Modulo Theories Website
SMT 2013, Helsinki, Finland - affiliated with SAT 2013
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