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

Abstract

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 - Dec 1 2006
Externally publishedYes
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
Volume1
ISSN (Print)1530-1591

Other

OtherDesign, Automation and Test in Europe, DATE'06
CountryGermany
CityMunich
Period3/6/063/10/06

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

  • Cite this

    Wang, C., Yang, Z., Ivančić, F., & Gupta, A. (2006). Disjunctive image computation for embedded software verification. In Proceedings - Design, Automation and Test in Europe, DATE'06 [1657077] (Proceedings -Design, Automation and Test in Europe, DATE; Vol. 1).