![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Datalog for Program Analysis: Beyond the Free Lunch
![]() Datalog for Program Analysis: Beyond the Free LunchAdd 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 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:
Note that ex-directory lists are not shown. |
Other listsLogic and Semantics Seminar (Computer Laboratory) Cambridge Centre for Climate ScienceOther talksBears, Bulls and Boers: Market Making and Southern African Mining Finance, 1894-1899 Double talk on Autism genetics Wetting and elasticity: 2 experimental illustrations Regulators of Muscle Stem Cell Fate and Function Cafe Synthetique: Synthetic Biology Industry Night |