BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From Bounded to Unbounded Proofs of Correctness - Aws Albarghouthi
 \, University of Toronto
DTSTART:20130411T101500Z
DTEND:20130411T111500Z
UID:TALK44196@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We describe automated techniques for proving program safety\, 
 that is\, proving that every execution of a program does not cause a crash
  (e.g.\, via division by zero) and satisfies intended functionality (e.g.\
 , a programmer-supplied assertion). The core idea underlying our approach 
 is that by examining a bounded version of the program\, with a finite numb
 er of execution paths\, we can generalize the proof of correctness to the 
 whole program. Our generalization capitalizes on advances in SMT solving f
 or path enumeration\, novel interpolant generation techniques for DAGs of 
 formulas\, and a tight integration with abstract domains in order to impro
 ve interpolant "quality". Our approach forms the basis of UFO\, a C verifi
 er we built in LLVM\, that has recently won numerous categories in the 201
 3 Competition on Software Verification (SV-COMP).
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR