Model checking sequential software programs via mixed symbolic analysis

Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivanĉić

Research output: Contribution to journalArticlepeer-review

11 Scopus citations


We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

Original languageEnglish (US)
Article number10
JournalACM Transactions on Design Automation of Electronic Systems
Issue number1
StatePublished - Jan 1 2009

All Science Journal Classification (ASJC) codes

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


  • Binary decision diagram
  • Composite symbolic formula
  • Image computation
  • Model checking
  • Presburger arithmetic
  • Reachability analysis


Dive into the research topics of 'Model checking sequential software programs via mixed symbolic analysis'. Together they form a unique fingerprint.

Cite this