Datalog for Program Analysis: Beyond the Free Lunch

Add to your list(s) Download to your calendar using vCal

• Mayur Naik, Georgia Institute of Technology
• Friday 16 August 2013, 14:00-15:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Recent years have witnessed widespread use of Datalog in expressing program analyses—programs that infer useful facts about other programs. Examples include analyses for proving security and concurrency properties of imperative programs. The benefits of Datalog, however, are currently limited to automating low-level implementation issues, such as efficient data structures and algorithms for executing these analyses. In particular, the task of finding an effective program abstraction—a central task that concerns balancing the scalability and accuracy of an analysis—is done manually by analysis designers. I will describe a new technique that lifts this limitation. The technique is based on counterexample-guided abstraction refinement which was developed in the model-checking community. 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 purpose in a manner that is general, complete, and optimal. I will discuss our experience applying this technique in the Chord framework to analyze real-world Java programs.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• personal list
• rp587

Note that ex-directory lists are not shown.