BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:IC3 Modulo Theories via Implicit Predicate Abstraction - Alberto G
 riggio\, Fondazione Bruno Kessler
DTSTART:20140326T140000Z
DTEND:20140326T150000Z
UID:TALK51518@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We present a novel approach for generalizing the IC3 algorithm
  for invariant checking from finite-state to infinite-state transition sys
 tems\, expressed over some background theories.  The procedure is based on
  a tight integration of IC3 with Implicit (predicate) Abstraction\, a tech
 nique that expresses abstract transitions without computing explicitly the
  abstract system and is incremental with respect to the addition of predic
 ates.  In this scenario\, IC3 operates only at the Boolean level of the ab
 stract state space\, discovering inductive clauses over the abstraction pr
 edicates.  Theory reasoning is confined within the underlying SMT solver\,
  and applied transparently when performing satisfiability checks.  When th
 e current abstraction allows for a spurious counterexample\, it is refined
  by discovering and adding a sufficient set of new predicates.  Importantl
 y\, this can be done in a completely incremental manner\, without discardi
 ng the clauses found in the previous search.\nThe proposed approach has tw
 o key advantages.  First\, unlike current SMT generalizations of IC3\, it 
 allows to handle a wide range of background theories without relying on ad
 -hoc extensions\, such as quantifier elimination or theory-specific clause
  generalization procedures\, which might not always be available\, and can
  moreover be inefficient.  Second\, compared to a direct exploration of th
 e concrete transition system\, the use of abstraction gives a significant 
 performance improvement\, as our experiments demonstrate.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR