BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Datalog for Program Analysis: Beyond the Free Lunch - Mayur Naik\,
  Georgia Institute of Technology
DTSTART:20130816T130000Z
DTEND:20130816T140000Z
UID:TALK46663@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Recent years have witnessed widespread use of Datalog in expre
 ssing program analyses -- programs that infer useful facts about other pro
 grams.  Examples include analyses for proving security and concurrency pro
 perties of imperative programs.  The benefits of Datalog\, however\, are c
 urrently limited to automating low-level implementation issues\, such as e
 fficient data structures and algorithms for executing these analyses.  In 
 particular\, the task of finding an effective program abstraction -- a cen
 tral task that concerns balancing the scalability and accuracy of an analy
 sis -- is done manually by analysis designers.  I will describe a new tech
 nique that lifts this limitation. The technique is based on counterexample
 -guided abstraction refinement which was developed in the model-checking c
 ommunity.  When a run of a Datalog analysis fails to prove a program fact 
 using the current abstraction\, our technique generalizes the cause of the
  failure to other abstractions\, and picks a new abstraction that avoids a
  similar failure.  It uses a boolean satisfiability solver for this purpos
 e in a manner that is general\, complete\, and optimal.  I will discuss ou
 r experience applying this technique in the Chord framework to analyze rea
 l-world Java programs.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR