Disjunctive image computation for software verification

Chao Wang, Zijiang Yang, Franjo Ivanvčić, Aarti Gupta

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


Existing BDD-based symbolic algorithms designed for hardware designs do not perform well on software programs. We propose novel techniques based on unique characteristics of software programs. Our algorithm divides an image computation step into a disjunctive set of easier ones that can be performed in isolation. We use hypergraph partitioning to minimize the number of live variables in each disjunctive component, and variable scopes to simplify transition relations and reachable state subsets. Our experiments on nontrivial C programs show that BDD-based symbolic algorithms can directly handle software models with a much larger number of state variables than for hardware designs.

Original languageEnglish (US)
Article number1230802
JournalACM Transactions on Design Automation of Electronic Systems
Issue number2
StatePublished - Apr 1 2007

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering


  • Binary decision diagram
  • Formal verification
  • Image computation
  • Model checking
  • Reachability analysis


Dive into the research topics of 'Disjunctive image computation for software verification'. Together they form a unique fingerprint.

Cite this