BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Making Prophecies with Decision Predicates - Eric Koskinen
DTSTART:20101129T124500Z
DTEND:20101129T140000Z
UID:TALK28175@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:We describe a new algorithm for proving temporal properties ex
 pressed\nin LTL of infinite-state programs.  Our approach takes advantage 
 of\nthe fact that LTL properties can often be proved more efficiently\nusi
 ng techniques usually associated with the branching-time logic CTL\nthan t
 hey can with native LTL algorithms.  The caveat is that\, in\ncertain inst
 ances\, nondeterminism in the system's transition relation\ncan cause CTL 
 methods to report counterexamples that are spurious with\nrespect to the o
 riginal LTL formula.  To address this problem we\ndescribe an algorithm th
 at\, as it attempts to apply CTL proof methods\,\nfinds and then removes p
 roblematic nondeterminism via an analysis on\nthe potentially spurious cou
 nterexamples.  Problematic nondeterminism\nis characterized using decision
  predicates\, and removed using a\npartial\, symbolic determinization proc
 edure which introduces new\nprophecy variables to predict the future outco
 me of these choices.  We\ndemonstrate---using examples taken from the Post
 greSQL database\nserver\, Apache web server\, and Windows OS kernel---that
  our method can\nyield enormous performance improvements in comparison to 
 known tools\,\nallowing us to automatically prove properties of programs w
 here we\ncould not prove them before.\n\n[This work is to appear in POPL 2
 011.]\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR