Using Declarative Languages for Fast and Easy Program Analysis

Date

August 3, 2009

Speaker

Yannis Smaragdakis

Affiliation

University of Massachusetts, Amherst

Overview

The talk will discuss the benefits of using logic-based declarative languages, especially for program analysis. The main focus will be on the Doop framework for points-to analysis of Java programs. Doop builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logic-based language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog and optimizing aggressively using a novel technique that takes into account Datalog incremental evaluation.

As a result, Doop decisively redefines the state-of-the-art in pointer analysis, and challenges our understanding of how to build scalable precise program analyses. Doop’s precise analyses are the first to achieve scalability without the use of binary decision diagrams (BDDs) and outperform BDD-based analyses by substantial amounts. We compare Doop with Lhot´ak and Hendren’s Paddle. For the exact same logical points-to definitions (and, consequently, identical precision) Doop is more than 15x faster than Paddle for common precise (context-sensitive) analyses of the DaCapo benchmarks. Additionally, Doop scales to very precise analyses that are impossible with Paddle and Whaley et al.’s bddbddb, directly addressing open problems in past literature. Finally, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness.

Generalizing from Doop and Datalog, we will discuss a broader plan for using declarative languages with a logical flavor for various domains in future work.

Speakers

Yannis Smaragdakis

Yannis Smaragdakis is an Associate Professor at the University of Oregon. His interests are in the areas of applied programming languages and software engineering. He got his B.S. degree from the University of Crete (Greece) and his Ph.D. from the University of Texas at Austin. He is a recipient of an NSF Career award, and “best paper” awards at ASE’07, ISSTA’06, GPCE’04, and USENIX’99. Yannis has authored numerous publications, and claims that “some are even good”.More information on his work can be found at: http://www.cs.uoregon.edu/~yannis