Static program transformations for efficient software model checking

Shobha Vasudevan, Jacob A. Abraham

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

Abstract

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
PublisherSpringer New York LLC
Pages257-281
Number of pages25
ISBN (Print)1402081561, 9781402081569
DOIs
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
Volume156
ISSN (Print)1868-4238

Other

OtherIFIP 18th World Computer Congress Topical Sessions
CountryFrance
CityToulouse
Period8/22/048/27/04

Keywords

  • 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

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

Cite this