=Paper=
{{Paper
|id=Vol-1163/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1163/preface.pdf
|volume=Vol-1163
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-1163/preface.pdf</pdf>
<pre>
Preface

This volume contains the papers presented at the 12th edition of the International Work-
shop on Satisfiability Modulo Theories (SMT 2014). The workshop was held on July 17th
and 18th 2014 as part of the Vienna Summer of Logic (VSL 2014), in association with the
26th International Conference on Computer Aided Verification (CAV 2014), the 7th Interna-
tional Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International
Conference on Theory and Applications of Satisfiability Testing (SAT 2014).
    The workshop is the main annual event of the SMT community, where both researchers
and users of SMT technology meet and discuss new theoretical ideas, implementation and
evaluation techniques, as well as applications. Like in previous editions of the workshop, this
year we invited submissions in three categories: extended abstracts, to present preliminary
reports of work in progress; original papers, to describe original and mature research; and
presentation-only papers, to provide additional access to important developments, recently
published or submitted elsewhere and which SMT Workshop attendees may be unaware of.
We received 13 submissions and each of them was reviewed by three program committee
members. Due to the quality of and interest in the submissions, and in keeping with the
desire to encourage presentation and discussion of work in progress, we were able to accept
11 contributions for presentation at the workshop: 2 original papers, 4 extended abstracts,
and 5 presentation-only papers. Furthermore, the program included two invited talks, by
Clark Barrett from New York University and Guillaume Melquiond from Inria. We would
like to thank the authors, the invited speakers, the program committee, and the reviewers
for their work and contributions to the workshop. We thank the CAV, IJCAR, SAT, and
VSL organizers for their support and for hosting the workshop, and the EasyChair team for
the availability of the EasyChair Conference System.


July, 2014                                                                  Philipp Rümmer
                                                                  Christoph M. Wintersteiger




                                               i
Table of Contents

 SMT: Where do we go from here? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
   Clark Barrett

 Speeding Up SMT-Based Quantitative Program Analysis . . . . . . . . . . . . . . . . . . . . . . . 3
    Daniel J. Fremont and Sanjit A. Seshia

 Multi-solver Support in Symbolic Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
   Hristina Palikareva and Cristian Cadar

 Protocol Log Analysis with Constraint Programming . . . . . . . . . . . . . . . . . . . . . . . . . . 17
    Mats Carlsson, Olga Grinchtein and Justin Pearson

 Reasoning About Set Comprehensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
    Edmund S. L. Lam and Iliano Cervesato

 Weakly Equivalent Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
   Juergen Christ and Jochen Hoenicke

 Decision Procedures for Flat Array Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
    Francesco Alberti, Silvio Ghilardi and Natasha Sharygina

 Extending SMT-LIB v2 with λ-Terms and Polymorphism . . . . . . . . . . . . . . . . . . . . . 53
    Richard Bonichon, David Déharbe and Cláudia Tavares

 Automating the Verification of Floating-Point Algorithms . . . . . . . . . . . . . . . . . . . . . 63
   Guillaume Melquiond

 Leveraging Linear and Mixed Integer Programming for SMT . . . . . . . . . . . . . . . . . . 65
    Tim King, Clark Barrett and Cesare Tinelli

 raSAT: SMT for Polynomial Inequality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
    To Van Khanh, Vu Xuan Tung and Mizuhito Ogawa

 Better Answers to Real Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
    Marek Kosta, Thomas Sturm and Andreas Dolzmann

 Towards Conflict-Driven Learning for Virtual Substitution . . . . . . . . . . . . . . . . . . . . 71
    Konstantin Korovin, Marek Kosta and Thomas Sturm




                                                                  iii
Program 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
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


Additional Reviewers
Aleksandar Zeljić




                                       v

</pre>