Colloquium Details

Logical Abstractions of Graphs

Speaker: Thomas Wies, Institute of Science and Technology, Austria

Location: Warren Weaver Hall 1302

Date: April 8, 2011, 11:30 a.m.

Host: Denis Zorin


Verification technology has proved useful for increasing software reliability and productivity. Its great asset lies in concepts and algorithms for the mechanical construction of formally precise, conservative abstractions of behavioral aspects of systems. Its applicability extends to other problems in Computer Science. A recent example is the use of abstraction algorithms for scheduling in cloud computing (implemented on top of Amazon's elastic compute cloud). In my talk, I will present techniques for computing and analyzing abstractions for systems whose behavior is expressed by (dynamically changing) graphs. Such systems are ubiquitous; one example are distributed systems in the actors framework of the Scala programming language. Our techniques are based on decision procedures for specific logical theories. The resulting logical abstractions of graphs give rise to a new generation of verification tools.


Refreshments will be offered starting 15 minutes prior to the scheduled start of the talk.

How to Subscribe