UK-Israel Bi-National Workshop

Verification of Infinite-State Systems

MAY 12-14, Tel Aviv University, Israel

Sponsored by the British Council and the Israeli Ministry of Sciences

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



Gideon Ariely (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




Cristiano Calcagno (Imperial College) tba

Nachum Dershowitz (Tel Aviv University) Commutation and Constriction

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

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

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) TBA

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) The 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

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