Helmut Veith Professor, Institut für Informatik, Technische Universität München

Environment Abstraction: Proving Ptolemy Right

Abstract:

In this talk, we describe environment abstraction, a new form of abstraction for parameterized systems. Characteristically, environment abstraction views a concurrent system from the point of view of a single process. We argue that for systems designed by human programmers this Ptolemaic view of the world yields precise and feasible abstract models. We survey examples of distributed algorithms and cache coherence protocols which were successfully verified by environment abstraction.

Joint Work with Ed Clarke and Muralidhar Talupur

Short Bio

Helmut Veith is a professor at the CS department of Munich Technical University, and an adjunct professor at Carnegie Mellon University. He holds a diploma in Computational Logic (1994) and a PhD "sub auspiciis praesidentis" in Computer Science (1998) from Vienna University of Technology. Prior to his appointment to Munich in 2003, he has hold positions at the assistant and associate professor levels in Vienna since 1995, and has been a visiting scientist at Carnegie Mellon University in 1999/2000. In his research, Helmut Veith applies formal and logical methods to problems in technical computer science and software technology. His current work is focussing on model checking, embedded systems, testing and computer security.