Program
October 3 – October 4 – October 5 – October 6
October 3 – Tutorials and Reception
| 8:00 – 9:00 | Registration and Continental Breakfast | |
| 9:00 – 10:15 |
Machine Learning and Systems
for the Next Frontier in Formal Verification Manish Pandey |
|
| 10:15 – 10:45 | Coffee Break | |
| 10:45 – 12:00 |
Verifying Hyperproperties of
Hardware Systems Bernd Finkbeiner and Markus Rabe |
|
| 12:00 – 14:00 | Lunch | |
| 14:00 – 15:15 |
A Paradigm Shift in
Verification Methodology Pranav Ashar |
|
| 15:15 – 15:45 | Coffee Break | |
| 15:45 – 17:00 |
Program Synthesis for
Networks Pavol Černý |
|
| 17:00 – … | Reception (held in Café A, Synopsys building A) |
October 4
| 8:00 – 8:50 | Continental Breakfast | |
| 8:50 – 9:00 | Welcome from the Chairs | |
| Keynote | ||
| 9:00 – 10:15 |
Formal Verification for
Computer Security: Lessons Learned and Future
Directions Dawn Song (Chair: Ruzica Piskac) |
|
| 10:15 – 10:45 | Coffee Break | |
|
Session 1: Program Synthesis
Chair: Chao Wang |
||
| 10:45 – 11:15 |
Synthesizing Adaptive Test Strategies from Temporal Logic
Specifications Roderick Bloem, Robert Koenighofer, Ingo Pill, and Franz Roeck |
|
| 11:15 – 11:45 |
SWAPPER: A Framework for Automatic Generation of Formula
Simplifiers based on Conditional Rewrite Rules Rohit Singh and Armando Solar-Lezama |
|
| 11:45 – 12:00 |
On ∃ ∀ ∃! Solving: A Case Study on
Automated Synthesis of Magic Card Tricks Susmit Jha, Vasumathi Raman, and Sanjit A. Seshia |
|
| 12:00 – 13:30 | Lunch | |
|
Session 2: Hardware Verification
Chair: Himanshu Jain |
||
| 13:30 – 14:00 |
Equivalence Checking Using Gröbner Bases Amr Sayed-Ahmed, Daniel Grosse, Mathias Soeken, and Rolf Drechsler |
|
| 14:00 – 14:30 |
Categorical Semantics of Digital Circuits Dan Ghica and Achim Jung |
|
| 14:30 – 15:00 |
Routing under Constraints Alexander Nadel |
|
| 15:00 – 15:30 | Coffee Break | |
|
Session 3: SMT Solving
Chair: Domagoj Babic |
||
| 15:30 – 16:00 |
Lazy Proofs for DPLL(T)-Based SMT Solvers Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, and Liana Hadarean |
|
| 16:00 – 16:30 |
Minimal unsatisfiable core extraction for SMT Ofer Guthmann, Ofer Strichman, and Anna Trostanetski |
|
| 16:30 – 17:00 |
Integrating Proxy Theories and Numeric Model Lifting for
Floating-Point Arithmetic Jaideep Ramachandran and Thomas Wahl |
|
| 17:00 – 17:30 |
Accurate ICP-based Floating-Point Reasoning Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, and Bernd Becker |
|
| Business Meeting | ||
| 17:30 – 18:00 | Business Meeting | |
October 5
| 8:00 – 9:00 | Continental Breakfast | |
|
Memorial Session for Helmut
Veith
Chair: Murali Talupur |
||
| 9:00 – 10:00 |
Memorial Session for Helmut Veith Talks by Anna Prianichnikova, Igor Konnov, Armin Biere, and Yuan Lu. |
|
| Keynote | ||
| 10:00 – 11:00 |
Understanding evolution
through algorithms Christos Papadimitriou (Chair: Murali Talupur) |
|
| 11:00 – 11:30 | Coffee Break | |
| Student Forum | ||
| 11:30 – 12:00 | Student Forum | |
| 12:00 – 13:30 | Lunch | |
|
Session 4: Protocols and Architecture Specifications
Chair: Igor Konnov |
||
| 13:30 – 14:00 |
Verifiable Hierarchical Protocols with Network Invariants on
Parametric Systems Opeoluwa Matthews, Jesse Bingham, and Daniel Sorin |
|
| 14:00 – 14:30 |
Modular Specification and Verification of a Cache-Coherent
Interface Kenneth McMillan |
|
| 14:30 – 15:00 |
Trustworthy Specifications of ARM v8-A and v8-M System Level
Architecture Alastair Reid |
|
| 15:00 – 15:30 |
Proof Certificates for SMT-based Model Checkers for
Infinite-state Systems Alain Mebsout and Cesare Tinelli |
|
| Banquet | ||
| 16:30 – 20:00 |
Banquet at Testarossa
Winery. Buses leave from the conference venue at 16:00 and return by approximately 20:30. See the Conference Venue page for more details. |
|
October 6
| 8:00 – 9:00 | Continental Breakfast | |
| Keynote | ||
| 9:00 – 10:00 |
Network Verification –
When Clarke Meets Cerf George Varghese (Chair: Alan Hu) |
|
| 10:00 – 10:30 | Coffee Break | |
|
Session 5: Networks and Industrial Applications
Chair: Georg Weissenbacher |
||
| 10:30 – 11:00 |
Optimizing Horn Solvers for Network Repair Hossein Hojjat, Philipp Ruemmer, Jedidiah McClurg, Pavol Černý, and Nate Foster |
|
| 11:00 – 11:30 |
Extracting Behaviour from an Executable Instruction Set
Model Brian Campbell and Ian Stark |
|
| 11:30 – 11:45 |
Combining Requirement Mining, Software Model Checking, and
Simulation-Based Verification for Industrial Automotive
Systems Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé, and Sanjit A. Seshia |
|
| 11:45 – 12:00 |
Formal Verification of Division and Square Root
Implementations, an Oracle Report David Rager, Jo Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Chau, and Ben Selfridge |
|
| 12:00 – 13:30 | Lunch | |
|
Session 6: Model Checking and Equivalence Checking
Chair: Armin Biere |
||
| 13:30 – 14:00 |
Property-Directed k-Induction Dejan Jovanović and Bruno Dutertre |
|
| 14:00 – 14:30 |
Efficient Uninterpreted Function Abstraction and Refinement
for Word-level Model Checking Yen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko, and Robert Brayton |
|
| 14:30 – 15:00 |
Reducing Interpolant Circuit Size by Ad Hoc Logic Synthesis
and SAT-Based Weakening Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini, and Danilo Vendraminetto |
|
| 15:00 – 15:30 |
Equivalence Checking By Logic Relaxation Eugene Goldberg |
|
| 15:30 – 16:00 | Coffee Break | |
|
Session 7: Concurrent and Timed Systems
Chair: Malay Ganai |
||
| 16:00 – 16:30 |
Soundness of the Quasi-Synchronous Abstraction Guillaume Baudart, Timothy Bourke, and Marc Pouzet |
|
| 16:30 – 17:00 |
Lazy Sequentialization for TSO and PSO via Shared Memory
Abstractions Ermenegildo Tomasco, Truc Nguyen Lam, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato |
|
| 17:00 – 17:30 |
Hybrid Partial Order Reduction with Under-Approximate
Dynamic Points-To and Determinacy Information Pavel Parizek |
|
| 17:30 – 18:00 |
A Consistency Checker for Memory Subsystem Traces Matthew Naylor, Simon Moore, and Alan Mujumdar |
|
| ～Fin～ | ||