PTA - BDD

Introduction

Documentation

Software

Sable Home

Points-To Analysis Using BDDs

Introduction top
In this project we investigated a new approach to solving a subset-based points-to analysis (Andersen's analysis) for Java using Binary Decision Diagrams (BDDs). In the model checking community, BDDs have been shown very effective for representing large sets and solving very large verification problems. Our work shows that BDDs can also be very effective for developing a points-to analysis that is simple to implement and that scales well, in both space and time, to large programs.

The design and evaluation is summarized in our PLDI'03 paper and our technical report.

Documentation top
  • new: PLDI 2003 paper, Presentation (June 17, 2003)

    Bibtex entry: 

    @inproceedings{bern.lhot.ea03,
  author        = "Marc Berndl and Ond\v{r}ej Lhot\'ak and Feng Qian and
		  Laurie Hendren and Navindra Umanee",
  title         = "Points-to analysis using BDDs",
  booktitle	= {Proceedings of the ACM SIGPLAN 2003 Conference on
		  Programming Language Design and Inplementation},
  year		= {2003},
  publisher	= {ACM Press}
  isbn          = {1-58113-662-5},
  pages         = {103--114},
  location      = {San Diego, California, USA},
  doi           = {http://doi.acm.org/10.1145/781131.781144},
  publisher     = {ACM Press}
}
  • Technical report
Software top
Snapshot of Nov. 15, 2002
  • code (which needs BuDDy package), and README first

    Copyright notice: 

                                     LICENSE
                                 -------
        A BDD Solver of Andersen's Points-to Analysis for Java
    Copyright (C) 2002 by Marc Berndl, Ondrej Lhotak and Feng Qian
                            All rights reserved

    Permission is hereby granted, without written agreement and without
    license or royalty fees, to use, reproduce, prepare derivative
    works, distribute, and display this software and its documentation
    for any purpose, provided that (1) the above copyright notice and
    the following two paragraphs appear in all copies of the source code
    and (2) redistributions, including without limitation binaries,
    reproduce these notices in the supporting documentation. Substantial
    modifications to this software may be copyrighted by their authors
    and need not follow the licensing terms described here, provided
    that the new terms are clearly indicated in all files where they apply.

    IN NO EVENT SHALL AUTHORS, OR DISTRIBUTORS OF THIS
    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

    AUTHORS SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
    MODIFICATIONS.

Note: The BuDDy library package is copyrighted by Jørn Lind-Nielsen.
  • benchmarks (constraints used as input to the solver)


Last updated Tue Jun 17 12:16:30 EDT 2003.