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

• Type: Conference
• Year: 2004
• Where: IFIP
• Authors: Shobha Vasudevan, Jacob A. Abraham
• Keywords: Abstraction Based Verification, Communications, IFIP 2004, Model Checking, Model Checking Problem