Decision diagrams for linear arithmetic

11 years 6 months ago
Decision diagrams for linear arithmetic
—Boolean manipulation and existential quantification of numeric variables from linear arithmetic (LA) formulas is at the core of many program analysis and software model checking es (e.g., predicate abstraction). We present a new data structure, Linear Decision Diagrams (LDDs), to represent formulas in LA and its fragments, which has certain properties that make it efficient for such tasks. LDDs can be seen as an extension of Difference Decision Diagrams (DDDs) to full LA. Beyond this extension, we make three key contributions. First, we extend sifting-based dynamic variable ordering (DVO) from BDDs to LDDs. Second, we develop, implement, and evaluate several algorithms for existential quantification. Third, we implement LDDs inside CUDD, a state-of-the-art BDD package, and evaluate them on a large benchmark consisting of 850 functions derived from the source code of 25 open source programs. Overall, our experiments indicate that LDDs are an effective data structure for program an...
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Authors Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Comments (0)