A New Approach to Temporal Property Verification

Presented as part of the 2012 HCSS conference.

Abstract:

I will describe a new approach to the old problem of automatic temporal property verification. As well as leading to dramatic performance improvements over existing techniques, this approach also brings some light to a couple of age-old questions.

Biography:

Dr. Byron Cook is a Principal Researcher at Microsoft Research Cambridge, as well as Professor of Computer Science at University College London.  His research interests focus on formal verification, theorem proving, operating systems, and biology.  Byron is particularly well known for his work on the Terminator program termination prover as well as the SLAM software model checker.  See http://research.microsoft.com/en-us/people/bycook/ for more information.