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.