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
StatePublished - Jan 1 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

Fingerprint

Model checking
Temporal logic
Formal methods
Syntactics
Explosions
Semantics
Software

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 and Management

Cite this

Vasudevan, S., & Abraham, J. A. (2004). Static program transformations for efficient software model checking. In Building the Information Society - IFIP 18th World Computer Congress Topical Sessions (pp. 257-281). (IFIP Advances in Information and Communication Technology; Vol. 156). Springer New York LLC.

Static program transformations for efficient software model checking. / Vasudevan, Shobha; Abraham, Jacob A.

Building the Information Society - IFIP 18th World Computer Congress Topical Sessions. Springer New York LLC, 2004. p. 257-281 (IFIP Advances in Information and Communication Technology; Vol. 156).

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

Vasudevan, S & Abraham, JA 2004, Static program transformations for efficient software model checking. in Building the Information Society - IFIP 18th World Computer Congress Topical Sessions. IFIP Advances in Information and Communication Technology, vol. 156, Springer New York LLC, pp. 257-281, IFIP 18th World Computer Congress Topical Sessions, Toulouse, France, 8/22/04.
Vasudevan S, Abraham JA. Static program transformations for efficient software model checking. In Building the Information Society - IFIP 18th World Computer Congress Topical Sessions. Springer New York LLC. 2004. p. 257-281. (IFIP Advances in Information and Communication Technology).
Vasudevan, Shobha ; Abraham, Jacob A. / Static program transformations for efficient software model checking. Building the Information Society - IFIP 18th World Computer Congress Topical Sessions. Springer New York LLC, 2004. pp. 257-281 (IFIP Advances in Information and Communication Technology).
@inproceedings{d80ad3190ea5460d9b11f8cc7f52862f,
title = "Static program transformations for efficient software model checking",
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.",
keywords = "Abstract interpretation, Abstraction, Amorphous slicing, Conditioned slicing, Counterexample based refinement, Data abstractions, Formal verification, Model checking, Program slicing, Strong/weak property preservation",
author = "Shobha Vasudevan and Abraham, {Jacob A.}",
year = "2004",
month = "1",
day = "1",
language = "English (US)",
isbn = "1402081561",
series = "IFIP Advances in Information and Communication Technology",
publisher = "Springer New York LLC",
pages = "257--281",
booktitle = "Building the Information Society - IFIP 18th World Computer Congress Topical Sessions",

}

TY - GEN

T1 - Static program transformations for efficient software model checking

AU - Vasudevan, Shobha

AU - Abraham, Jacob A.

PY - 2004/1/1

Y1 - 2004/1/1

N2 - 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.

AB - 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.

KW - Abstract interpretation

KW - Abstraction

KW - Amorphous slicing

KW - Conditioned slicing

KW - Counterexample based refinement

KW - Data abstractions

KW - Formal verification

KW - Model checking

KW - Program slicing

KW - Strong/weak property preservation

UR - http://www.scopus.com/inward/record.url?scp=62349123320&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=62349123320&partnerID=8YFLogxK

M3 - Conference contribution

SN - 1402081561

SN - 9781402081569

T3 - IFIP Advances in Information and Communication Technology

SP - 257

EP - 281

BT - Building the Information Society - IFIP 18th World Computer Congress Topical Sessions

PB - Springer New York LLC

ER -