BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Craig Interpretation - Aws Albarghouthi\, University of Toronto
DTSTART:20120910T130000Z
DTEND:20120910T140000Z
UID:TALK39462@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Abstract interpretation is one of the most scalable and automa
 ted approaches to program verification available today. To achieve efficie
 ncy\, many steps of the analysis (e.g.\, join and widening) lose precision
 \, thus producing false alarms.\n\nIn this talk\, I will describe VINTA\, 
 an iterative algorithm for refining the results of abstract interpretation
  using Craig Interpolants and SMT solvers. Craig interpolants are used to 
 recover the imprecision lost by abstract interpretation and guide the sear
 ch towards a safe inductive invariant\, or a real bug.\n \nWe have impleme
 nted VINTA in the LLVM compiler infrastructure and applied it to benchmark
 s from the software verification competition. Our results show that VINTA 
 out-performs state-of-the-art verification tools. \n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR