Title: Compositional Reasoning for Parameterized Verification

Speaker: Murali Talupur

Place: 32-G531

Time: 1-2:30pm

Date: Friday, September 19, 2008

Abstract:"
Distributed protocols like cache coherence protocols form the bedrock on
which modern multiprocessor systems are built. Such distributed
protocols are typically designed parametrically, that is, independent of
the precise number of processors involved. Given that distributed
programs are hard to reason about for humans and that no amount of
testing/simulation can cover all scenarios, it becomes necessary that we
find methods to formally and parametrically verify the correctness of
such systems.  In this talk we will describe a promising method based on
compositional reasoning that has been successfully applied to verify
large cache coherence protocols and on going extensions to it.