BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Coming to Grips with Complexity in Computer-Aided Verification - K
 enneth McMillan\, Microsoft Research Redmond
DTSTART:20110609T130000Z
DTEND:20110609T140000Z
UID:TALK31686@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Model Checking was introduced in the 1980's\, providing a full
 y automated way to verify that a finite-state system satisfies a logical s
 pecification\, or to generate a behavioral counterexample showing that it 
 doesn't. Model checking could verify (and sometimes find surprising bugs i
 n) simple protocols and digital circuits. Making model checking into an ef
 fective tool for engineers has been a long process\, however\, and has req
 uired us to come to grips with the complexity of real circuits and systems
  (which in model checking manifests itself as the "state explosion problem
 ").\n\nIn this talk\, I'll focus on one key aspect of this many-faceted pr
 oblem\, namely the question of relevance. That is\, how can we abstract ou
 t just the relevant facts about a system for proving a given property\, wh
 ile ignoring large amounts of irrelevant information?\n\nIt turns out that
  quite a bit has been learned about this question over the last decade\, e
 specially from the study of the Boolean satisfiability problem. We have le
 arned how to produce relevant generalizations from special cases using ded
 uction\, and to focus on relevant facts by tightly coupling search and ded
 uction.\nIn the process\, some surprising connections arisen with classica
 l results in proof theory (Craig's interpolation lemma) and more recent re
 sults in proof complexity\, allowing us to exploit the explanatory power o
 f machine-generated proofs. \n\nThese ideas have given us a toe-hold on th
 e issue of relevance\, and this in turn has allowed far more complex syste
 ms to be automatically verified using model checking. This more than any o
 ther factor has made it possible for engineers to apply model checking to 
 real chip designs\, and for model checking to be applied to software.\n\nI
 'll give a high-level overview of these developments\, trying to draw out 
 some of the fundamental ideas\, pointing to some of the broader implicatio
 ns and some future possibilities.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR