Strachey Lecture in Computer Science

The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking

On 11th May 2010 (Week 3, Trinity Term), we are delighted to welcome Professor O Grumberg (TECHNION, Israel Institute of Technology) to give a Strachey Lecture.  This will be held at 16:30 in Lecture Theatre B, and there will be tea and cakes in the Atrium beforehand.

Abstract 

Model checking is a widely used technique for automatic verification of hardware and software systems. Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems.

Abstraction is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is refined by adding some of the hidden details back.

In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed.

Finally, we will mention some applications of TVAR.

About the Strachey Lecture Series

This is a termly series of Distinguished Lectures named after Christopher Strachey, the first Professor of Computation at Oxford University.

Christopher Strachey was the first leader of the Programming Research Group (PRG), part of the Oxford University Computing Laboratory (OUCL), founded in 1965. He was the first Professor of Computation at Oxford, succeeded by Sir Tony Hoare in 1977 after his untimely death. With Dana Scott he founded the field of denotational semantics, providing a firm mathematical foundation for programming languages.

Click here to see details of previous Strachey Lectures