Welcome to the LinDD Project

This project is dedicated to Linear Decision Diagrams (LDDs) and associated tools and techniques. LDD is a data structure for representing formulas in linear arithmetic (LA) and its fragments. It is designed to be efficient for tasks that are at the core of many program analysis and software model checking techniques (e.g., predicate abstraction). Such tasks include Boolean manipulation and existential quantification of numeric variables from LA formulas. LDDs can be seen as an extension of Difference Decision Diagrams (DDDs) to full LA, and are implemented on top of the state-of-the-art CUDD package. Below you will find links to LDD-related documents and software releases.

Publications

• Decision Diagrams for Linear Arithmetic, Sagar Chaki, Arie Gurfinkel, Ofer Strichman, Proceedings of Formal Methods in Computer-Aided Design (FMCAD), page 53-60, November 15-18, 2009. PDF Online Presentation
• BOXES: A Symbolic Abstract Domain of Boxes, Arie Gurfinkel, Sagar Chaki, Proceedings of the 17th International Static Analysis Symposium (SAS), September 14-16, 2010. PDF

Software

• ldd : The LDD library. Implementation is in C, and on top of CUDD.
• lddsolver : A solver for SMT formulas built on top of LDD.
  • Source code. An Eclipse project. See LddsolverEclipseTutorial.
  • Standalone binary. For usage information, run:

    java -jar lddsolver.jar
    

    Typical usage:

    java -jar lddsolver.jar -t tvpi --exists fm foo.smt
    

Benchmarks

Each benchmark is a set of SMT formulas with existential quantification. Goal is to compute equivalent formulas without quantifiers. Available benchmarks are:

• fmcad09_benchmark : Each SMT formula represents a forward image computation. Used in our FMCAD09 paper (see publications above).
• pa : Each SMT formula represents a predicate abstraction query for large-block encoding.

License

The software is distributed under a modified BSD License (LddLicense)

Contact

Email lindd-feedback@… with questions and comments.