Friday, July 1, 2016 (room 17A)
| 08:50 - 9:00 | Opening Remarks Tim King and Ruzica Piskac |
Session: Building an SMT solver Chair: Tim King | |
| 09:00 - 10:00 | The Nuts and Bolts of Yices (Invited Talk)
(slides) Bruno Dutertre |
| 10:00 - 10:30 | LOIS: an application of SMT solvers
(slides) Eryk Kopczynski and Szymon Toruńczyk |
| 10:30 - 11:00 | Coffee break - 2nd floor |
Session: Reasoning about Bit-Vectors Chair: Pascal Fontaine | |
| 11:00 - 11:30 | Deciding Bit-Vector Formulas with mcSAT
(slides) Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer |
| 11:30 - 12:00 | Z3str2+BV: A Solver for a Theory of Strings and Bit-vectors
(slides) Murphy Berzish, Sanu Subramanian, Yunhui Zheng, Omer Tripp and Vijay Ganesh |
| 12:00 - 12:30 | On Intervals and Bounds in Bit-vector Arithmetic
(slides) Mikolas Janota and Christoph M. Wintersteiger |
| 12:30 - 14:00 | Lunch - Centro Clutural D. Dinis (CCDD) |
Session: Constraint Programming Chair: Ruzica Piskac | |
| 14:00 - 15:00 | Constraint Programming - an Introduction, with some Applications to String Processing (Invited Talk)
(slides) Justin Pearson |
| 15:00 - 15:30 | Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
(slides) Jeevana Priya Inala, Rohit Singh and Armando Solar-Lezama |
| 15:30 - 16:00 | Coffee break - 2nd floor |
Session: Interfaces & Problem Encoding Chair: Philipp Ruemmer | |
| 16:00 - 16:30 | Clause Sharing and Partitioning for Cloud-Based SMT Solving
(slides) Matteo Marescotti, Antti Hyvärinen and Natasha Sharygina |
| 16:30 - 17:00 | On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT
(slides) Roberto Sebastiani and Patrick Trentin |
| 17:00 - 17:30 | Scrambling and Descrambling SMT-LIB Benchmarks
(slides) Tjark Weber |
Saturday, July 2, 2016 (room 17A)
Session: Termination analysis Chair: Tim King | |
| 09:00 - 10:00 | SMT Techniques and Solvers in Automated Termination Analysis (Invited Talk)
(slides) Carsten Fuhs |
| 10:00 - 10:30 | Kneecap: Model-based Generation of Network Traffic
(slides) Nik Sultana and Richard Mortier |
| 10:30 - 11:00 | Coffee break - 2nd floor |
Session: Theoretical Foundations Chair: Roberto Sebastiani | |
| 11:00 - 11:30 | Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
(slides) Martin Bromberger and Christoph Weidenbach |
| 11:30 - 12:00 | Satisfiability Modulo Free Data Structures Combined with Bridging Functions
(slides) Raphael Berthon and Christophe Ringeissen |
| 12:00 - 12:30 | Reasoning with Sets and Sums of Sets
(slides) Markus Bender |
| 12:30 - 14:00 | Lunch - Centro Clutural D. Dinis (CCDD) |
Session: Practical Applications Chair: Jasmin Blanchette | |
| 14:00 - 14:30 | MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
(slides) Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati and Krzysztof Czarnecki |
| 14:30 - 15:00 | Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis
(slides) Peter Backeman, Christoph M. Wintersteiger, Boyan Yordanov and Sara-Jane Dunn |
| 15:00 - 15:30 | Proof Certificates for SMT-based Model Checkers
(slides) Alain Mebsout and Cesare Tinelli |
| 15:30 - 16:00 | Coffee break - 2nd floor |
Session: Business Meeting Chairs: Tim King and Ruzica Piskac | |
| 16:00 - 16:30 | SMT-COMP'16 Report (slides) |
| 16:30 - 17:00 | SMT-LIB Updates and Discussion |
| 17:00 - 17:30 | Business Meeting |
