University of Cambridge > > Microsoft Research Cambridge, public talks > Datalog for Program Analysis: Beyond the Free Lunch

Datalog for Program Analysis: Beyond the Free Lunch

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

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 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity