Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Proving Ptolemy Right: Environment Abstraction for Concurrent Systems

  • Speaker:   Prof  Helmut Veith  (TU Munich)
  • Host:   Andrei Voronkov
  • 28th February 2007 at 14:15 in 1.5
Concurrent systems are notoriously error-prone and hard to analyze, both for human engineers and verification tools. In this talk, we describe environment abstraction, a method for automated verification of concurrent systems with an unbounded number of processes. In environment abstraction, the abstract state space describes properties of the concurrent system from the point of view of individual processes. We argue that for systems designed by human programmers this Ptolemaic viewpoint yields precise and feasible abstract models. We present examples of distributed algorithms and cache coherence protocols which where successfully verified by enviromnent abstraction.
▲ Up to the top