University of Minnesota
Software Engineering Center

You are here

Improving Symbolic Execution for Statecharts Formalisms

Date of Publication: 
September 2012
Associated Research Groups: 
Publication Files: 
Symbolic execution is a program analysis technique that attempts to explore all possible paths through a program by using symbolic values rather than actual data values as inputs. When applied to Statecharts, a model-based formalism for reactive systems, symbolic execution can determine all feasible paths through a model up to a specified bound and generate input sequences exercising these paths. The main drawback of this method is its computational expense. This paper describes two efforts to improve the performance of symbolic execution within our previously developed framework for Statechart analysis. One method is a multithreaded symbolic execution engine targeted directly at our framework. A second, orthogonal, method is program specialization with respect to a particular model and Statechart semantics, which uses symbolic execution to rewrite the original code into an equivalent form that has fewer instructions and is easier to analyze.
MoDeVVa '12 Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation
@inproceedings{Balasubramanian:2012:ISE:2427376.2427385, author = {Balasubramanian, Daniel and P\u{a}s\u{a}reanu, Corina and Whalen, Michael W. and Karasi, G\'{a}bor and Lowry, Michael}, title = {Improving symbolic execution for statechart formalisms}, booktitle = {Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation}, series = {MoDeVVa '12}, year = {2012}, isbn = {978-1-4503-1801-3}, location = {Innsbruck, Austria}, pages = {47--52}, numpages = {6}, publisher = {ACM}, address = {New York, NY, USA} }