Program

October 2 – October 3 – October 4 – October 5 – October 6

October 2 – Tutorials and Reception

9:30 – 10:00	Registration & Coffee
9:50 – 10:00	Welcome session
10:00 – 12:00	How Formal Methods and Analysis Helps Security of Entire Blockchain-based Systems Shin’ichiro Matsuo
12:00 – 13:30	Lunch
13:30 – 15:30	Symbolic Security Analysis using the Tamarin Prover Cas Cremers
15:30 – 16:00	Coffee Break
16:00 – 18:00	Consistency Properties of Parallel/Distributed Programs in cat Jade Algave
19:30 –	Reception in the City Hall (how to get there)

October 3

8:30 – 9:00	Registration
8:50 – 9:00	Welcome session
9:00 – 10:00	Keynote: Formal Verification, Model Checking, and Constraints for Security of the Cloud Byron Cook
10:00 – 10:15	Coffee Break
10:15 – 10:45	Student Forum
Session 1: Arithmetic Chair: Yakir Vizel
10:45 – 11:00	Tool paper: goSAT: Floating-point Satisfiability as Global Optimization M. Ammar Ben Khadra, Dominik Stoffel and Wolfgang Kunz
11:00 – 11:30	On Sound Relative Error Bounds for Floating-Point Arithmetic Anastasiia Izycheva and Eva Darulova
11:30 – 12:00	Column-Wise Verification of Multipliers Using Computer Algebra Daniela Ritirc, Armin Biere and Manuel Kauers
12:00 – 13:30	Lunch
Session 2: Solving Chair: Armin Biere
13:30 – 14:00	Efficient Generation of All Minimal Inductive Validity Cores Elaheh Ghassabani, Michael Whalen and Andrew Gacek
14:00 – 14:30	Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions Leonardo Alt, Antti Hyvärinen, Sepideh Asadi and Natasha Sharygina
14:30 – 15:00	Solving Linear Arithmetic with SAT-based Model Checking Yakir Vizel, Alexander Nadel and Sharad Malik
15:00 – 15:15	Tool paper: Z3str3: A String Solver with Theory-aware Heuristics Murphy Berzish, Yunhui Zheng and Vijay Ganesh
15:15 – 15:45	Coffee Break
Session 3: Concurrency and Distributed Systems Chair: Florian Zuleger
15:45 – 16:15	Verification of a lazy cache coherence protocol against a weak memory model Christopher Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson and Vijay Nagarajan
16:15 – 16:45	Safety Verification of Phaser Programs Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
16:45 – 17:15	Learning to prove safety over parameterised concurrent systems Anthony Widjaja Lin, Yu-Fang Chen, Chih-Duo Hong and Philipp Ruemmer
17:15 – 17:45	Lasso detection using Partial State Caching Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal and Shaz Qadeer
Business Meeting
17:45 – 18:15	Business Meeting
19:00 –	PC Dinner

October 4

9:00 – 10:00	Keynote: Formal Methods in Industrial Dependable Systems Design - The TTTech Example Wilfried Steiner
10:00 – 10:15	Coffee Break
10:15 – 10:45	Student Forum
Session 4: Probabilistic Systems Chair: Doron Peled
10:45 – 11:15	Exact Quantitative Probabilistic Model Checking Using Rational Search Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan
11:15 – 11:45	Sampling Invariants from Frequency Distributions Grigory Fedyukovich, Samuel Kaufman and Rastislav Bodik
11:45 – 12:30	Student Posters
12:00 – 13:30	Lunch
Session 5: BDDs Chair: Andreas Griesmayer
13:30 – 14:00	Tagged BDDs: Combining reduction rules from different decision diagram types Tom van Dijk, Robert Wille and Robert Meolic
14:00 – 14:30	First-order Temporal Logic Monitoring with BDDs Klaus Havelund, Doron Peled and Dogan Ulus
14:30 – 15:00	Factored Boolean Functional Synthesis Lucas Martinelli Tabajara and Moshe Y. Vardi
15:00 – 15:15	Coffee Break
15:15 – 15:45	Student Posters
15:45 – 18:00	Social Event: Museum Visit (guided tour at 16:30, leave from Kuppelsaal at 15:45; meet at ticket center of Upper Belvedere at 16:15)
18:30 –	Conference banquet at Salm Bräu

October 5

Session 6: IC3 (Part 1) Chair: Natasha Sharygina
9:00 – 9:30	Property Directed Reachability with Word-Level Abstraction Yen-Sheng Ho, Alan Mishchenko and Robert Brayton
9:30 – 10:00	Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris
10:00 – 10:30	K-Induction without Unrolling Arie Gurfinkel and Alexander Ivrii
10:30 – 11:00	Coffee Break
Session 7: IC3 (Part 2) Chair: Alexander Ivrii
11:00 – 11:30	Designing Parallel PDR Matteo Marescotti, Arie Gurfinkel, Antti Hyvärinen and Natasha Sharygina
11:30 – 12:00	FuseIC3: An Algorithm for Checking Large Design Spaces Rohit Dureja and Kristin Yvonne Rozier
12:00 – 12:15	Tool paper: FAR-Cubicle – A new reachability algorithm Mattias Roux, Sylvain Conchon, Sava Krstic, Rupak Majumdar and Amit Goel
12:15 – 12:30	Tool paper: Theta: a Framework for Abstraction Refinement-Based Model Checking Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei and István Majzik
12:30 – 13:30	Lunch
13:30 – 14:00	Hardware Model Checking Competition 2017 (HWMCC'17)
Session 8: Hybrid Systems Chair: Mirco Giacobbe
14:00 – 14:30	Modular SMT-Based Analysis of Nonlinear Hybrid Systems Kyungmin Bae and Sicun Gao
14:30 – 15:00	SMT-based Analysis of Switching Multi-Domain Linear Kirchhoff Networks Alessandro Cimatti, Sergio Mover and Mirko Sessa
15:00 – 15:30	Coffee Break
Session 9: Applications (1) Chair: Per Bjesse
15:30 – 16:00	Automatic Verification of Application-Tailored OSEK Kernels Hans-Peter Deifel, Christian Dietrich, Merlin Göttlinger, Daniel Lohmann, Stefan Milius and Lutz Schröder
16:00 – 16:30	Estimating Worst-case Latency of on-chip Interconnects with Formal Simulation Freek Verbeek and Nike van Vugt-Hage
16:30 – 17:00	Coffee Break
Session 10: Applications (2) Chair: Igor Konnov
17:00 – 17:30	Parameterized Verification of Algorithms for Oblivious Robots on a Ring Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru and Sebastien Tixeuil
17:30 – 18:00	Automated Analysis and Repair By Example for Firewalls William Hallahan, Ennan Zhai and Ruzica Piskac

October 6 – Helmut Veith Symposium

Note that the Symposium takes place in a different building (in walking distance from the main building; see details here).

9:00 – 9:30	Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
9:30 – 10:00	On Compiling Boolean Circuits Optimized for Secure Multi-party Computation Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Helmut Veith
10:00 – 10:30	Shield Synthesis Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Robert Könighofer, Ufuk Topcu
10:30 – 11:00	Coffee Break
11:00 – 11:30	Program Synthesis for Interactive-Security Systems William Harris, Somesh Jha, Thomas Reps, Sanjit Seshia
11:30 – 12:00	A Methodology to Take Credit for High-Level Verification During RTL Verification Frederic Doucet, R. P. Kurshan
12:00 – 12:15	Grab a sandwich
12:15 – 13:15	LogicLounge (LogicLunch)