TODAYS EVENTS (addition)

[David Melski <melski@xxxxxxxxxxx>]

2:15 pm, 1207 CS
PL Seminar: Tom Ball, Microsoft Research, "On the Relative Completeness of
   counterexample-driven Refinement"

We consider whether a program verification method known as ``software
model checking with iterated abstraction refinement'' (as implemented
in the SLAM project) is complete relative to fixpoint iteration with
``oracle-guided'' widening.  We show that whenever backward fixpoint
iteration with oracle-guided widening succeeds in proving a property P
(for some sequence of widenings determined by the oracle) then
software model checking with a particular form of iterated backward
refinement will succeed in proving P.  Intuitively, this means that
the use of fixpoint iteration over abstractions and a particular
iterated backwards refinement of the abstractions has the effect of
exploring the entire state space of all possible sequences of
widenings.

(Joint work with Andreas Podelski and Sriram. K. Rajamani)

http://research.microsoft.com/slam/