BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Coming to Grips with Complexity in Computer-Aided 
 Verification - Kenneth McMillan\, Microsoft Resear
 ch Redmond
DTSTART;TZID=Europe/London:20110609T140000
DTEND;TZID=Europe/London:20110609T150000
UID:TALK31686AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/31686
DESCRIPTION:Model Checking was introduced in the 1980's\, prov
 iding a fully automated way to verify that a finit
 e-state system satisfies a logical specification\,
  or to generate a behavioral counterexample showin
 g that it doesn't. Model checking could verify (an
 d sometimes find surprising bugs in) simple protoc
 ols and digital circuits. Making model checking in
 to an effective tool for engineers has been a long
  process\, however\, and has required us to come t
 o grips with the complexity of real circuits and s
 ystems (which in model checking manifests itself a
 s the "state explosion problem").\n\nIn this talk\
 , I'll focus on one key aspect of this many-facete
 d problem\, namely the question of relevance. That
  is\, how can we abstract out just the relevant fa
 cts about a system for proving a given property\, 
 while ignoring large amounts of irrelevant informa
 tion?\n\nIt turns out that quite a bit has been le
 arned about this question over the last decade\, e
 specially from the study of the Boolean satisfiabi
 lity problem. We have learned how to produce relev
 ant generalizations from special cases using deduc
 tion\, and to focus on relevant facts by tightly c
 oupling search and deduction.\nIn the process\, so
 me surprising connections arisen with classical re
 sults in proof theory (Craig's interpolation lemma
 ) and more recent results in proof complexity\, al
 lowing us to exploit the explanatory power of mach
 ine-generated proofs. \n\nThese ideas have given u
 s a toe-hold on the issue of relevance\, and this 
 in turn has allowed far more complex systems to be
  automatically verified using model checking. This
  more than any other factor has made it possible f
 or 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 th
 ese developments\, trying to draw out some of the 
 fundamental ideas\, pointing to some of the broade
 r implications and some future possibilities.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7
  J J Thomson Avenue (Off Madingley Road)\, Cambrid
 ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR