| Time | Speaker | Title (Click for Abstract) |
|---|---|---|
| 9:00-9:20 | Greetings | |
| 9:20-10:00 | Ofer Strichman (Technion) | Beyond Vacuity: Towards the Strongest Passing Formula |
| 10:00-10:20 | Break | |
| 10:20-11:00 | Michael Huth (Imperial College) | PCTL Model Checking of Markov Chains: Truth and Falsity as Winning Strategies in Games |
| 11:00-11:20 | Break | |
| 11:20-12:00 | Noam Rinetzky (Queen Mary University of London) | Abstraction for Concurrent Objects |
| 12:00-14:00 | Lunch Break | |
| 14:00-14:40 | Orna Kupferman (Hebrew University) | Reasoning about Online Algorithms with Weighted Automata |
| 14:40-15:00 | Break | |
| 15:00-15:40 | Luke Ong (Oxford University) | Recursion Schemes, Types and Model-Checking Functional Programs |
| 15:40-16:00 | Break | |
| 16:00-16:40 | Alexander Rabinovich (Tel Aviv University) | Extensions of the Church Synthesis problem |
| Time | Speaker | Title (Click for Abstract) |
|---|---|---|
| 9:10-9:50 | Doron Peled (Bar Ilan University) | Priority Scheduling of Distributed Systems Based on Model Checking |
| 9:50-10:10 | Break | 10:10-10:50 | Kousha Etessami (University of Edinburgh) | Adding Recursion to Markov Chains, Markov Decision Processes, and Stochastic Games |
| 10:50-11:10 | Break | |
| 11:10-11:50 | James Worrel (Oxford U.) | Reachability in Succinct and Parametric One-Counter Automata |
| 11:50-12:30 | Dov Gabbay (King's College and Bar Ilan University) | Reactive Automata |
| 12:30-14:00 | Lunch Break | |
| 14:00-14:40 | Nachum Dershowitz (Tel Aviv University) | Mortality in Infinite-State Systems |
| 14:40-15:00 | Break | |
| 15:00-15:40 | Joel Ouaknine (Oxford University) | Time-Bounded Verification |
| 15:40-16:00 | Break | |
| 16:00-16:40 | Yoram Hirshfeld (Tel Aviv University) | Real-Time Temporal Logics |
| Time | Speaker | Title (Click for Abstract) |
|---|---|---|
| 9:10-9:50 | Orna Grumberg (Technion) | 3-Valued Abstraction in (Bounded) Model Checking for Hardware |
| 9:50-10:30 | Ranko Lazic (University of Warwick) | The covering and boundedness problems for branching vector addition systems |
| 10:30-10:50 | Break | |
| 10:50-11:30 | Cristiano Calcagno (Imperial College) | Compositional Shape Analysis by means of Bi-Abduction |
| 11:30-12:10 | Shmuel Katz (Technion) | Using Dataflow to Avoid Model Checking for Aspects |
| Closing and Lunch |