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.