Background

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





Aims 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

Following the initiative started at PDPAR'06, there are two categories of submissions:

  • 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, we will welcome work in progress and novel ideas that are not yet competitive in practice.

  • 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 both 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

  • Submission deadline: April 28th, 2007
  • Notification of acceptance/rejection: May 28th, 2007
  • Final version due: June 4th, 2007
  • Workshop: July 1st-2nd, 2007




Programme committee














Previous editions





Invited speakers

  • Rupak Majumdar (University of California, Los Angeles)

  • Title: Proofs and Counterexamples

    Abstract: Finding precise yet small abstractions automatically has been one of the biggest challenges in software verification. In this talk, I shall outline some recent work in generating abstractions automatically through the analysis of counterexample traces. Decision procedures play a fundamental role in this process, both to check whether a counterexample is genuine or spurious, and to generate abstract explanations in case the counterexample is spurious. Conversely, algorithms for counterexample analysis have influenced the interface exposed by a modern decision procedure: in addition to a "yes/no" decision, the decision procedure must produce proofs of unsatisfiability and interpolants.


  • Peter O'Hearn (Quen Mary, University of London)

  • Title: Proof Procedures for Separated Heap Abstractions

    Abstract: Separation logic is a program logic geared towards reasoning about programs that mutate heap-allocated data structures. This talk describes ideas arising from joint work with Josh Berdine and Cristiano Calcagno on proof procedure for a sublogic of separation logic that is oriented to lightweight program verification and analysis. The proof theory uses ideas from substructural logic together with induction-free reasoning about inductive definitions of heap structures. Substructural reasoning is used to to infer frame axioms, which describe the portion of a heap that is not altered by a procedure, as well as to discharge verification conditions; more precisely, the leaves of failed proofs can give us candidate frame axioms. Full automation is achieved through the use of special axioms that capture properties that would normally be proven using by induction.

    I will illustrate the proof method through its use in the Smallfoot static assertion checker, where it is used to prove verification conditions and infer frame axioms, as well as in the Space Invader program analysis, where it is used to accelerate the convergence of fixed-point calculations.




Program

[Download proceedings]

Sunday, July 1st:


09:30   INVITED TALK: Peter O'Hearn (Queen Mary, University of London)
Proof Procedures for Separated Heap Abstractions [slides]


10:30‑11:00  Coffee Break

11:00   Zvonimir Rakamaric, Roberto Bruttomesso, Alan Hu and Alessandro Cimatti.
Deciding Unbounded Heaps in an SMT Framework.[slides]
11:30   Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and Daniele Zucchelli.
Combination Methods for Model-Checking of Infinite-State Systems.[slides]
12:00   Leonardo de Moura and Nikolaj Bjorner.
Model-based Theory Combination.[slides]


12:30‑14:00  Lunch break

14:00   Michal Moskal, Jakub Lopuszanski and Joseph Kiniry.
E-matching For Fun And Profit.[slides]
14:30   Yeting Ge, Clark Barrett and Cesare Tinelli.
Solving Quantified Verification Conditions using Satisfiability Modulo Theories.[slides]
15:00   Leonardo de Moura and Nikolaj Bjorner
Efficient E-matching for SMT Solvers[slides]


15:30‑16:00  Coffee break

16:00   Panel discussion on input languages
17:00   Business meeting


Monday, July 2nd:


09:30   INVITED TALK: Rupak Majumdar (University of California, Los Angeles)
Proofs and Counterexamples [slides]


10:30‑11:00  Coffee Break

11:00   Jeremy Bongio, Cyrus Katrak, Hai Lin, Ralph Eric McGregor, Christopher Lynch and Yuefeng Tang.
Encoding First Order Proofs in SMT.[slides]
11:30   Sylvain Conchon, Evelyne Contejean and Johannes Kanig.
CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers.[slides]
12:00   Ofer Strichman and Mirron Rozanov.
Generating minimum transitivity constraints in P-time for deciding Equality Logic.[slides]


12:30‑14:00  Lunch break
14:00   SMT-COMP tool presentations

15:30‑16:00  Coffee break
16:00   SMT-COMP tool presentations and SMT-COMP discussion




Student travel awards

SMT 2007 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 chair by May 28.





Sponsors

SMT 2007 recognizes the generous support of the following companies: