Generalized Symbolic Execution for Model Checking and Testing

@incollection{citeulike:3037858, abstract = {Modern software systems, which often are concurrent and manipulate complex data structures must be extremely reliable. We present a novel framework based on symbolic execution, for automated checking of such systems. We provide a two-fold generalization of traditional symbolic execution based approaches. First, we define a source to source translation to instrument a program, which enables standard model checkers to perform symbolic execution of the program. Second, we give a novel symbolic execution algorithm that handles dynamically allocated structures (e.g., lists and trees), method preconditions (e.g., acyclicity), data (e.g., integers and strings) and concurrency. The program instrumentation enables a model checker to automatically explore different program heap configurations and manipulate logical formulae on program data (using a decision procedure). We illustrate two applications of our framework: checking correctness of multi-threaded programs that take inputs from unbounded domains with complex structure and generation of non-isomorphic test inputs that satisfy a testing criterion. Our implementation for Java uses the Java PathFinder model checker.}, author = {Khurshid, Sarfraz and P\u{a}s\u{a}reanu, Corina and Visser, Willem }, citeulike-article-id = {3037858}, journal = {Tools and Algorithms for the Construction and Analysis of Systems}, keywords = {model\_checking, symbolic\_execution}, pages = {553--568}, posted-at = {2008-07-23 22:59:38}, priority = {2}, title = {Generalized Symbolic Execution for Model Checking and Testing}, url = {http://dx.doi.org/10.1007/3-540-36577-X\_40}, year = {2003} }

TY - CHAP ID - citeulike:3037858 L3 - citeulike-article-id:3037858 TI - Generalized Symbolic Execution for Model Checking and Testing JF - Tools and Algorithms for the Construction and Analysis of Systems SP - 553 EP - 568 N2 - Modern software systems, which often are concurrent and manipulate complex data structures must be extremely reliable. We present a novel framework based on symbolic execution, for automated checking of such systems. We provide a two-fold generalization of traditional symbolic execution based approaches. First, we define a source to source translation to instrument a program, which enables standard model checkers to perform symbolic execution of the program. Second, we give a novel symbolic execution algorithm that handles dynamically allocated structures (e.g., lists and trees), method preconditions (e.g., acyclicity), data (e.g., integers and strings) and concurrency. The program instrumentation enables a model checker to automatically explore different program heap configurations and manipulate logical formulae on program data (using a decision procedure). We illustrate two applications of our framework: checking correctness of multi-threaded programs that take inputs from unbounded domains with complex structure and generation of non-isomorphic test inputs that satisfy a testing criterion. Our implementation for Java uses the Java PathFinder model checker. KW - model_checking KW - symbolic_execution AU - Khurshid, Sarfraz AU - Păsăreanu, Corina AU - Visser, Willem PY - 2003/// UR - http://dx.doi.org/10.1007/3-540-36577-X_40 ER -