BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Backward Analysis via Over-Approximate Abstraction and Under-Appro
 ximate Subtraction - Alexey Bakhirkin\, MSR/University of Leicester
DTSTART:20140822T150000Z
DTEND:20140822T160000Z
UID:TALK53897@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:We propose a novel approach for computing weakest liberal safe
  preconditions of programs. The standard approaches\,\nwhich call for eith
 er under-approximation of a greatest fixed point\, or complementation of a
  least fixed point\, are\noften difficult to apply successfully. Our appro
 ach relies on a different decomposition of the weakest precondition\nof lo
 ops. We exchange the greatest fixed point for the computation of a least f
 ixed point above a recurrent set\,\ninstead of the bottom element. Converg
 ence is achieved using over-approximation\, while in order to maintain sou
 ndness\nwe use an under-approximating logical subtraction operation. Unlik
 e general complementation\, subtraction more easily\nallows for increased 
 precision in case its arguments are related. The approach is not restricte
 d to a specific\nabstract domain and we use it to analyze programs using t
 he abstract domains of intervals and of 3-valued structures.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR