Logical Abstractions for Verification

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 our 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 depends on complex states,
such as distributed message passing systems in the actors framework.
Our techniques are based on decision procedures for specific logical
theories. The resulting logical abstractions give rise to a new
generation of verification tools.