Program Day 1 - Tuesday 14/11/2017

08:30 - 09:30 Registration and Welcome

09:30 - 09:45 Opening Remarks

09:45 - 10:45 Keynote: QED and Symbolic QED: Dramatic Improvements in Pre-silicon and Post-silicon Validation of Digital Systems
Prof. Subhasish Mitra, Department of Electrical Engineering and Department of Computer Science, Stanford University
View keynote slides
Session chair: Avi Ziv

10:45 - 11:45 Technical Session: Modeling
Session chair: Marijn Heule

A Framework for Asynchronous Circuit Modeling and Verification in ACL2,
Cuong Chau, Warren Hunt, Marly Roncken, and Ivan Sutherland

Modeling undefined behaviour semantics for checking equivalence across compiler optimizations,
Manjeet Dahiya and Sorav Bansal

11:45 - 12:15 Coffee Break

12:15 - 13:15 Technical Session: Concurrency analysis
Session chair: Shmuel Katz

Deferrability Analysis for JavaScript,
Johannes Kloos, Rupak Majumdar and Frank McCabe

A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models,
Tatsuya Abe

13:15 - 14:30 Lunch

14:30 - 15:30 Keynote: Scalable, Transparent and Post-quantum Secure Computational Integrity, with applications to Crypto-currencies
Prof. Eli Ben-Sasson, Department of Computer Science, Technion - Israel Institute of Technology
Session chair: Ofer Strichman

15:30 - 17:00 Technical Session: Security and testing
Session chair: Cristian Cadar

Trace-based Analysis of Memory Corruption Malware Attacks,
Zhixing Xu, Aarti Gupta and Sharad Malik

Trace-Based Run-time Analysis of Message-Passing Go Programs,
Martin Sulzmann and Kai Stadtmuller

Software Verification: Testing vs. Model Checking. A Comparative Evaluation of the State of the Art,
Dirk Beyer and Thomas Lemberger

17:10 - 18:30 Reception, Posters and Tool Demos