Static program transformations for efficient software model checking

Shobha Vasudevan, Jacob A. Abraham

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


Ensuring correctness of software by formal methods is a very relevant and widely studied problem. Automatic verification of software using model checking suffers from the state space explosion problem. Abstraction is emerging as the key candidate for making the model checking problem tractable, and a large body of research exists on abstraction based verification. Many useful abstractions are performed at the syntactic and semantic levels of programs and their representations. In this paper, we explore abstraction based verification techniques that have been used at the program source code level. We provide a brief survey of these program transformation techniques. We also examine, in some detail, Program Slicing, an abstraction technique that holds great promise when dealing with complex software. We introduce the idea of using more specialized forms of slicing, Conditioned Slicing and Amorphous Slicing, as program transformation based abstractions for model checking. Experimental results using conditioned slicing for verifying safety properties written in temporal logic show the promise of these techniques.

Original languageEnglish (US)
Title of host publicationBuilding the Information Society - IFIP 18th World Computer Congress Topical Sessions
Number of pages25
ISBN (Print)1402081561, 9781402081569
StatePublished - 2004
Externally publishedYes
EventIFIP 18th World Computer Congress Topical Sessions - Toulouse, France
Duration: Aug 22 2004Aug 27 2004

Publication series

NameIFIP Advances in Information and Communication Technology
ISSN (Print)1868-4238


OtherIFIP 18th World Computer Congress Topical Sessions


  • Abstract interpretation
  • Abstraction
  • Amorphous slicing
  • Conditioned slicing
  • Counterexample based refinement
  • Data abstractions
  • Formal verification
  • Model checking
  • Program slicing
  • Strong/weak property preservation

ASJC Scopus subject areas

  • Information Systems
  • Computer Networks and Communications
  • Information Systems and Management


Dive into the research topics of 'Static program transformations for efficient software model checking'. Together they form a unique fingerprint.

Cite this