Programme

Saturday, July 18
Chair: Vijay Ganesh
8:45 – 9:00 Opening
9:00 – 10:00 Invited Talk: Margus Veanes
Strings and Automata Modulo Theories
[slides]
10:00 – 10:30 Break
Chair: Christoph Wintersteiger
10:30 – 11:00 Alexander Nadel and Nachum Dershowitz
Is Bit-Vector Reasoning as Hard as NExpTime in Practice? [slides]
11:00 – 11:30 Liana Hadarean, Ruben Martins, Martin Brain and Daniel Kroening
Stronger, Better, Faster: Optimally Propagating SAT Encodings [slides]
11:30 – 12:00 Bruno Dutertre
Solving Exists/Forall Problems With Yices [slides]
12:00 – 13:30 Lunch
Chair: Bruno Dutertre
13:30 – 14:30 Invited Talk: Cristian Cadar
Constraint Solving in Symbolic Execution
[slides]
14:30 – 15:00 Marco Gario and Andrea Micheli
PySMT: a Solver-Agnostic Library for Fast Prototyping of SMT-Based Algorithms [slides]
15:00 – 15:30 Break
Chair: Pascal Fontaine
15:30 – 16:00 Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli
Model Finding for Recursive Functions in SMT [slides]
16:00 – 16:30 Sam Bayless, Noah Bayless, Holger Hoos and Alan J. Hu
SAT Modulo Monotonic Theories [slides]
16:30 – 17:00 Richard Bonichon, David Déharbe, Pablo Federico Dobal and Cláudia Tavares
SMTpp: preprocessors and analyzers for SMT-LIB [slides]
Sunday, July 19
Chair: Sylvain Conchon
9:00 – 10:00 Invited Talk: John Regehr
Compiler Optimizations and SMT
10:00 – 10:30 Break
Chair: Alberto Griggio
10:30 – 11:00 Joe Hendrix and Ben Jones
Bounded Integer Linear Constraint Solving via Lattice Search [slides]
11:00 – 11:30 Martin Bromberger, Thomas Sturm and Christoph Weidenbach
Linear Integer Arithmetic Revisited [slides]
11:30 – 12:00 Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Mani Srivastava and Paulo Tabuada
Imhotep-SMT: A Satisfiability Modulo Theory Solver For Secure State Estimation [slides]
12:00 – 13:30 Lunch
Chair: Andrew Reynolds
13:30 – 14:00 Andreas Fellner, Pascal Fontaine, Georg Hofferek and Bruno Woltzenlogel Paleo
NP-completeness of small conflict set generation for congruence closure [slides]
14:00 – 14:30 Liana Hadarean, Alex Horn and Tim King
A Concurrency Problem with Exponential DPLL(T) Proofs [slides]
14:30 – 15:00 Stéphane Graham-Lengrand
Slot Machines: an approach to the Strategy Challenge in SMT solving [slides]
15:00 – 15:30 Break
Chair: Dejan Jovanović
15:30 – 16:00 SMT Competition [slides]
16:00 – 17:00 SMT-LIB Discussion
17:00 – 17:30 Bussiness Meeting