====================================================================== ------------------ 2nd Call for Papers ------------------- SMT Workshop '07 5th International Workshop on Satisfiability Modulo Theories Previously called: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) Berlin, Germany, 1-2 July 2007 (affiliated with CAV '2007) http://www.lsi.upc.edu/~oliveras/smt07 ====================================================================== 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 the workshop is to bring together researchers and users of SMT tools and techniques. Continuing with the PDPAR tradition, we especially encourage submission of papers focused on pragmatic aspects. Relevant topics include but are not limited to: * New decision procedures and new theories of interest * Combination of decision procedures * Novel implementation techniques * Benchmarks and evaluation methodologies * Applications and case studies * Theoretical results Important dates ~~~~~~~~~~~~~~~ Submission deadline : 23 April Notification of acceptance/rejection : 21 May Final version due : 4 June Workshop : 1-2 July Proceedings ~~~~~~~~~~~ Given the informal style 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. Paper Submission and Proceedings ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Following the PDPAR'06 initiative, 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 in both categories will be peer-reviewed. Papers should not exceed 10 pages (Postscript or PDF) and should be written in LaTeX, 11pt, one column, a4paper, standard margins. Technical details may be included in an appendix to be read at the reviewers' discretion. Full submission guidelines are at the workshop web page. Invited Speakers ~~~~~~~~~~~~~~~~ - Rupak Majumdar, University of California, Los Angeles. - Peter O'Hearn, Queen Mary, University of London. 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, students in other situations are also encouraged to apply. We require applications in the form of a short recommendation letter written by the student's supervisor, to be sent to the PC chairs by May 28. Program Chairs ~~~~~~~~~~~~~~ - Sava Krstic, Intel Corporation - Albert Oliveras, Tech. Univ. of Catalonia Program Committee ~~~~~~~~~~~~~~~~~ Clark Barrett, New York University Alessandro Cimatti, ITC-Irst, Trento Byron Cook, Microsoft Research Amit Goel, Intel Corporation Aarti Gupta, NEC Labs America Shuvendu Lahiri, Microsoft Research Leonardo de Moura, Microsoft Research Robert Nieuwenhuis, Technical University of Catalonia Silvio Ranise, LORIA, Nancy Roberto Sebastiani, Universita` di Trento Ofer Strichman, Technion Cesare Tinelli, University of Iowa Ashish Tiwari, Stanford Research Institute (SRI)