| 9:00-9:05 | Opening and Welcome (PC Chairs) |
||
Session 1 |
Session Chair : Sandrine Blazy | ||
| 9:00-10:00 | Invited talk | Advanced Development of Certified OS Kernels | Zhong Shao (Yale University) |
| 10:00-10:30 | Regular paper | Relational Program Reasoning Using Compiler IR | Moritz Kiefer, Vladimir Klebanov and Mattias Ulbrich. |
| 10:30-11:00 | Break |
||
| 11:00-12:30 | Session 2 (short papers) |
Session Chair : Richard Trefler | |
| The Matrix Reproved | Martin Clochard, Léon Gondelman and Mário Pereira | ||
| Producing All Ideals of a Forest, Formally | Jean-Christophe Filliâtre and Mário Pereira | ||
| JavaSMT: A Unified Interface for SMT Solvers in Java | Egor Karpenkov, Dirk Beyer and Karlheinz Friedberger | ||
| Enabling Modular Verification with Abstract Interference Specifications for a Concurrent Queue | Alan D. Weide, Murali Sitaraman and Paolo A. G. Sivilotti. | ||
| Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs | Steven Stewart, Derek Rayside, Vijay Ganesh and Krzysztof Czarnecki. | ||
| 12:30-14:00 | Lunch |
||
Session 3 |
Session Chair : Temesghen Kahsai | ||
| 14:00-15:00 | Invited talk | Automating Software Analysis at Large Scale | Michael Tautschnig, Amazon |
| 15:00-15:30 | Regular paper | Automated Verification of Functional Correctness of Race-Free GPU Programs | Kensuke Kojima, Akifumi Imanishi and Atsushi Igarashi |
| 15:30-16:00 | Break and demos (outside BA1190) |
||
Session 4 |
Session Chair : Marsha Chechik | ||
| 16:00-17:00 | Invited talk | RACE to Build Highly Concurrent and Distributed Systems | Oksana Tkachuk, NASA Ames/SGT |
| 17:00-17:30 | Regular paper | Order Reduction for Multi-Core Preemptive Operating Systems | Jonas Oberhauser |
Session 5 |
Session Chair : Temesghen Kahsai | ||
| 9:00-10:00 | Invited talk | Specification: The Biggest Bottleneck in Formal Methods and Autonomy | Kristin Rozier |
| 10:00-10:30 | Regular paper | Constructing Semantic Models of Programs with The Software Analysis Workbench | Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee and Aaron Tomb |
| 10:30-11:00 | Break |
||
| 11:00-12:30 | Session 6 (regular papers) |
Session Chair : Kristin Rozier | |
| SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms | Dirk Beyer and Matthias Dangl | ||
| Resolution in Solving Graph Problems | Kailiang Ji | ||
| 12:30-14:00 | Lunch |
||
Session 7 |
Session Chair : Sandrine Blazy | ||
| 14:00-15:00 | Invited talk | Formally Checking Safety Cases for a Radiotherapy Machine | Zachary Tatlock, University of Washington |
| 15:00-15:30 | Regular paper | Bidirectional Grammars for Machine-Code Decoding and Encoding | Gang Tan and Greg Morrisett |
| 15:30-16:00 | Break and demos (outside BA1190) |
||
Session 8 |
Session Chair : Marsha Chechik | ||
| 16:00-17:00 | Invited talk | Stupid Tool Tricks for Smart Model Based Design | Mark Lawford, McMaster |
| 17:00-17:05 | Closing |