Disjunctive image computation for embedded software verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations


Finite state models generated from software programs have unique characteristics that are not exploited by existing model checking algorithms. In this paper, we propose a novel disjunctive image computation algorithm and other simplifications based on these characteristics. Our algorithm divides an image computation into a disjunctive set of easier ones that can be performed in isolation. Hypergraph partitioning is used to minimize the number of live variables in each disjunctive component. We use the live variables to simplify transition relations and reachable state subsets. Our experiments on a set of real-world C programs show that the new algorithm achieves orders-of-magnitude performance improvement over the best known conjunctive image computation algorithm.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE'06
StatePublished - 2006
EventDesign, Automation and Test in Europe, DATE'06 - Munich, Germany
Duration: Mar 6 2006Mar 10 2006

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
ISSN (Print)1530-1591


OtherDesign, Automation and Test in Europe, DATE'06

All Science Journal Classification (ASJC) codes

  • General Engineering


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

Cite this