Verification Day 2016

Time and place: Wednesday 1/6/2016, Tel Aviv University

Program

9:00 - 9:10 – Gathering

9:10 - 9:15 – Welcome

9:15 - 10:15 – Session I   (Yaglom Auditorium, The Senate Building)

Karam Abdelkader (Technion): Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. [Slides]

Shaull Almagor (HUJI): The Sensing Cost of Synthesis. [Slides]

Kalev Alpernas (TAU): Some Complexity Results for Stateful Network Verification. [Slides]

10:15 - 11:00 – Break

11:00 - 12:00 – Session II   (Yaglom Auditorium, The Senate Building)

Oded Padon (TAU): Ivy: Safety Verification by Interactive Generalization. [Slides]

Yotam Feldman (TAU): Verifying Expressive Inductive Invariants by Bounded-Horizon Instantiations. [Slides]

Adi Sosnovich (Technion): Analyzing Internet Routing Security Using Model Checking. [Slides]

Ofer Guthmann (Technion): Minimal Unsatisfiable Core Extraction for SMT. [Slides]

12:00 - 13:00 – Lunch, Yaglom Auditorium

13:00 - 14:00 – Session III   (Wolfson Engineering building, room 206)

Yair Nof (Technion): Real Time Solving of Online Discrete Optimization Problems. [Slides]

Jan Oliver Ringert (TAU): On Well-Separation of GR(1) Specifications. [Slides]

Or Pistiner (TAU): Symbolic BDD and ADD Algorithms for Energy Games. [Slides]

Aviv Kuvent (TAU): On Debugging Unrealizable GR(1) Specifications. [Slides]

14:00 - 14:30 ­– Break

14:30 - 15:30 – Session IV   (Wolfson Engineering building, room 206)

Gal Vardi (HUJI): On Relative and Probabilistic Finite Counterability. [Slides]

Maor Veitsman (Technion): Regression Verification for Unbalanced Recursive Functions. [Slides]

Yaniv David (Technion): Statistical Similarity of Binaries. [Slides]

Assaf Marron (Weizmann): Towards Wise Computing: An Initial Wise Development Environment for Behavioral Models. [Slides]