SMT 2008
6th International Workshop on Satisfiability Modulo Theories
July 7-8, 2008
Princeton, USA
Background
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be useful in verification, compiler optimization, scheduling, and other areas.
The success of SMT techniques depends on the development of both domain-specific decision procedures for each concrete 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. These two ingredients together make SMT techniques well-suited for use in larger automated reasoning and formal verification efforts.
Aim and Scope
The aim of this workshop is to bring together researchers working on SMT and users of SMT techniques. Relevant topics include but are not limited to:
- New decision procedures and new theories of interest
- Combinations of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Applications and case studies
- Theoretical results
Papers on pragmatical aspects of implementing and using SMT tools are especially encouraged.
Submission and Call for Papers
There are three categories of submissions:
- Extended abstracts: Extended abstracts: contain
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 but not in the ENTCS
archive.
- 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. Given the informal style of the workshop,
work in progress will be welcome.
- 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 should be submitted using the automated submission system
Papers in all categories will be peer-reviewed. Submitted papers
(PDF or PostScript) should not exceed 10 pages and should be written
in LaTeX with the following settings: 11pt, one column, a4paper and
standard margins. The paper may include, in addition, an appendix
containing technical details, which reviewers may read or not, at
their discretion.
Call for papers: [txt | pdf].
Electronic submission: Submission is via EasyChair (thanks to Andrei Voronkov).
Proceedings
Given the informal nature of the workshop,
only informal proceedings will be distributed
at the workshop.
We are planning to publish a selected subset of the submitted papers
as post-proceedings in a special volume of the Electronic
Notes in Theoretical Computer Science (ENTCS) unless the authors
prefer not to.
Important dates
- Extended submission deadline: April 30th, 2008
- Notification of acceptance/rejection: May 28th, 2008
- Final version due: June 4th, 2008
- Workshop: July 7-8, 2008
Programme committee
Previous editions
Invited speakers
Student travel awards
SMT 2008 will partially reimburse some students for their
conference-related expenses. Preference will be given to students
playing an active role in the workshop. However, also students in
other other situation are encouraged to apply.
Applications consist of a short recommendation letter by the student's
supervisor to be sent to the PC chairs by May 28.
Program
Monday, July 7th:
- 8:45 Opening Remarks
- 9:00 Using SMT solvers for deductive verification of
C and Java programs (invited talk), Jean-Christophe Filliâtre (slides).
- 10:00 Implementing Polymorphism in SMT solvers, Evelyne Contejean, Sylvain Conchon, Stéphane Lescuyer and Francois Bobot (slides).
10:30 - 11:00 Break I
- 11:00 Cover Algorithms and Their Combination, Sumit Gulwani and Madanlal Musuvathi (slides).
- 11:20 SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers, Germain Faure, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez Carbonell (slides).
- 11:40 An algebraic approach for the unsatisfiability of nonlinear constraints, Ashish Tiwari.
- 12:00 Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra, Christoph Scholl, Stefan Disch and Florian Pigorsch (slides).
12:30 - 2:00 Lunch
- 2:00 Efficient Interpolant Generation in Satisfiability Modulo Theories, Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani (slides).
- 2:20 Rocket-Fast Proof Checking for SMT Solvers, Michal Moskal.
- 2:40 Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report, Yeting Ge and Clark Barrett (slides).
- 3:00 Towards an SMT Proof Format, Aaron Stump and Duckki Oe (slides).
3:30 - 4:00 Break II
- 4:00 SMT-LIB panel
- 5:00 Business meeting
Tuesday, July 8th:
- 9:00 Reasoning about Arrays (invited talk), Aaron Bradley (slides).
- 10:00 Lemmas on Demand for the Extensional Theory of Arrays, Robert Brummayer and Armin Biere (slides).
10:30 - 11:00 Break I
- 11:00 Towards SMT Model Checking of Array-based Systems, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and Daniele Zucchelli (slides).
- 11:20 Back to the future: Revisiting Precise Program Verification using SMT solvers, Shuvendu Lahiri and Shaz Qadeer.
- 11:40 SMELS: Satisfiability Modulo Equality with Lazy Superposition, Christopher Lynch and Duc-Khanh Tran (slides).
- 12:00 Deciding Array Formulas with Fruagal Axiom Instantiation, Amit Goel, Sava Krstic and Alexander Fuchs (slides).
12:30 - 1:30 Lunch
- 1:30 Pex - White Box Test Generation for .NET (invited talk), Nikolai Tillmann (slides).
- 2:30 SMT-COMP panel
3:30 - 4:00 Break II
- 4:00 SMT-COMP tool presentations
Sponsors
SMT 2008 recognizes the generous support of the following companies:
