Background
Deciding the satisfiability of firstorder 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 domainspecific decision procedures for each concrete theory (e.g. linear arithmetic, the theory of arrays, or the theory of bitvectors) and combination methods that allow one to obtain more versatile SMT tools. These two ingredients together make SMT techniques wellsuited 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.
 Presentationonly 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 peerreviewed. 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.
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 postproceedings 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 1st2nd, 2007
Programme committee


Previous editions
Invited speakers
Rupak Majumdar (University of California, Los Angeles)
Title: Proofs and Counterexamples
Peter O'Hearn (Quen Mary, University of London)
Title: Proof Procedures for Separated Heap Abstractions
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.
Abstract: Separation logic is a program logic geared towards reasoning about programs that mutate heapallocated 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 inductionfree 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 fixedpoint calculations.
Program
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 ModelChecking of InfiniteState Systems.[slides] 
12:00  Leonardo de Moura and Nikolaj Bjorner. Modelbased Theory Combination.[slides] 
12:30‑14:00 Lunch break
14:00  Michal Moskal, Jakub Lopuszanski and Joseph Kiniry. Ematching 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 Ematching 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 Ptime for deciding Equality Logic.[slides] 
12:30‑14:00 Lunch break
14:00  SMTCOMP tool presentations 
15:30‑16:00 Coffee break
16:00  SMTCOMP tool presentations and SMTCOMP discussion 
Student travel awards
SMT 2007 will partially reimburse some students for their conferencerelated 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: