UK-Israel Bi-National Workshop

Verification of Infinite-State Systems

MAY 12-14, Tel Aviv University, Israel

Under the Auspices of the
Ministry of Science & Technology, Israel
British Council Israel

The workshop's themes include

Software verification, Parameterised systems, Timed and probabilistic systems. Symbolic data structures for representing infinite state spaces, Temporal logics, Separation logic, Shape analysis, Rewrite systems, Dynamic and mobile networks, Abstraction-refinement techniques, Games on infinite structures, Controller synthesis, Systems with dynamic memory and infinite data domains

For the schedule click PROGRAM


Gideon Ariely (Israeli Ministry of Science)
Sarit Atias (Israeli Ministry of Science)
Nachum Dershowitz (Tel Aviv University)
Orna Grumberg (Technion)
Orna Kupferman (Hebrew University)
Doron Peled (Bar Ilan University)
Alexander Rabinovich (Tel Aviv University), Chair




Tel - Aviv Travel Guide


Cristiano Calcagno (Imperial College) Compositional Shape Analysis by means of Bi-Abduction

Nachum Dershowitz (Tel Aviv University) Mortality in Infinite-State Systems

Kousha Etessami (University of Edinburgh) Adding Recursion to Markov Chains, Markov Decision Processes, and Stochastic Games

Dob Gabbay (King’s College and Bar Ilan University) Reactive Automata

Orna Grumberg (Technion) 3-Valued Abstraction in (Bounded) Model Checking for Hardware

Yoram Hirshfeld (Tel Aviv University) Process Algebras

Michael Huth (Imperial College) PCTL Model Checking of Markov Chains: Truth and Falsity as Winning Strategies in Games

Shmuel Katz (Technion) Using Dataflow to Avoid Model Checking for Aspects

Orna Kupferman (Hebrew University) Reasoning about Online Algorithms with Weighted Automata

Ranko Lazic (University of Warwick) The covering and boundedness problems for branching vector addition systems

Luke Ong (Oxford University) Recursion Schemes, Types and Model-Checking Functional Programs

Doron Peled ((Bar Ilan University) Priority Scheduling of Distributed Systems Based on Model Checking

Joel Ouaknine (Oxford University) Time-Bounded Verification

Alexander Rabinovich (Tel Aviv University) Extensions of the Church synthesis problem

Noam Rinetzky (Queen Mary University of London) Abstraction for Concurrent Objects

Ofer Strichman (Technion) Beyond Vacuity: Towards the Strongest Passing Formula

Boaz Trakhtenbrot (Tel Aviv University) TBA

James Worrell (Oxford University) Reachability in Succinct and Parametric One-Counter Automata