Sciweavers

Share
IFIP
2004
Springer

Static program transformations for efficient software model checking

10 years 1 months ago
Static program transformations for efficient software model checking
Ensuring correctness of software by formal methods is a very relevant and widely studied problem. Automatic verification of software using model checkers 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. 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 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 stractions for model checking. Experimental results using conditioned slicin...
Shobha Vasudevan, Jacob A. Abraham
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where IFIP
Authors Shobha Vasudevan, Jacob A. Abraham
Comments (0)
books