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
Synopsis:
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.
Notes:
In-person attendance only available to those with active NYU ID cards.