Generalized Symbolic Execution for Model Checking and Testing Export

@inproceedings{Khurshid03, 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 di\#erent 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.}, author = {Khurshid, Sarfraz and Pasareanu, Corina S. and Visser, Willem}, booktitle = {In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, citeulike-article-id = {5942173}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862}, keywords = {execution, symbolic}, pages = {553--568}, posted-at = {2009-10-15 02:53:45}, priority = {2}, title = {Generalized Symbolic Execution for Model Checking and Testing}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862}, year = {2003} }

TY - CONF ID - Khurshid03 L3 - citeulike-article-id:5942173 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 di#erent 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. EP - 568 TI - Generalized Symbolic Execution for Model Checking and Testing T2 - In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems SP - 553 KW - execution KW - symbolic AU - Khurshid, Sarfraz AU - Pasareanu, Corina AU - Visser, Willem PY - 2003/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862 ER -