Name
Abstract | ||
|---|---|---|
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 techniques (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 analysis tasks. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/FMCAD.2009.5351143 | 2009 Formal Methods in Computer-Aided Design |
Keywords | Field | DocType |
Boolean manipulation,linear arithmetic formula,program analysis technique,software model checking technique,linear decision diagrams,difference decision diagrams,open source programs,dynamic variable ordering | Boolean function,Data structure,Existential quantification,Predicate abstraction,Source code,Computer science,Theoretical computer science,Boolean algebra,Program analysis,Benchmark (computing) | Conference |
Citations | PageRank | References |
13 | 0.69 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sagar Chaki | 1 | 687 | 41.58 |
| Arie Gurfinkel | 2 | 939 | 55.15 |
| Ofer Strichman | 3 | 1071 | 63.61 |