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 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:
- 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.
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
- Clark Barrett, New York University
- Guillaume Melquiond, Université Paris Sud
Programme committee
- Martin Brain (University of Oxford)
- Roberto Bruttomesso (Atrenta)
- Bruno Dutertre (SRI international)
- Pascal Fontaine (Inria, Loria, University of Lorraine)
- Malay Ganai (NEC Labs America)
- Sicun Gao (Carnegie Mellon University)
- Amit Goel (Calypto Design Systems)
- Alberto Griggio (FBK-IRST)
- Jochen Hoenicke (University of Freiburg)
- Dejan Jovanović (SRI international)
- Albert Oliveras (Technical University of Catalonia)
- Philipp Rümmer (Uppsala University) - co-chair
- Christoph Sticksel (The University of Iowa)
- Cesare Tinelli (The University of Iowa)
- Tjark Weber (Uppsala University)
- Georg Weissenbacher (Vienna University of Technology)
- Thomas Wies (New York University)
- Christoph M. Wintersteiger (Microsoft Research) - co-chair
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? (Slides) |
| 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 (Slides) |
| 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:
- Extended abstracts: 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 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 relevant for the SMT community that has recently been published or submitted at other venues. They will not be included in the proceedings.
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
- Submission deadline: April 13th, 2014 EXTENDED to April 23rd, 2014
- Notification: May 20th, 2014
- Camera ready versions due: May 27th, 2014
- Workshop: July 17-18, 2014
Related events
- The 4th SAT/SMT Summer School, taking place July 10-12, just before FLoC.
- The Satisfiability Modulo Theories Competition SMT-COMP 2014
- The 26th CAV conference
- The 7th IJCAR conference
- The 17th SAT conference
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