Formal Methods in Software Engineering

Path Directed Symbolic Execution in the K Framework

Year2010
TypeConference
StatusPostproceedings
AuthorsIrina Asavoae, Mihail Asavoae, Dorel Lucanu

Links

Abstract

The K framework is a rewrite-based executable semantic framework built with the purpose to define programming languages and formal analysis methods. This paper introduces K definition of the path-directed symbolic execution, which is that part of Counterexample Guided Abstraction Refinement (CEGAR) where the counterexample is checked for spuriousness. To express this technique in K, we use strongest post condition computation on straight line code. The programming language at hand is imperative, with simple arithmetic, but the approach can be applied to more complicated languages. This work aims to further advance the integration of CEGAR technique in rewriting logic semantics project in general, and in K in particular. By doing this we obtain an uniform description of the definition of the programming language, the abstract model checking, and the counterexample guided refinement. This uniformity enables formal reasoning about CEGAR's implementation correctness which could be further standardized and eventually automatized.

BibTeX

@inproceedings{AsavoaeAL10, author = {Irina Mariuca Asavoae and Mihail Asavoae and Dorel Lucanu}, title = {Path Directed Symbolic Execution in the K Framework}, booktitle = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010, Timisoara, Romania, 23-26 September 2010}, year = {2010}, pages = {133-141}, publisher = {IEEE Computer Society}, isbn = {978-0-7695-4324-6}, editor = {Tetsuo Ida and Viorel Negru and Tudor Jebelean and Dana Petcu and Stephen M. Watt and Daniela Zaharie}, ee = {http://dx.doi.org/10.1109/SYNASC.2010.78}, url = {http://synasc10.info.uvt.ro/[SYNASC]}, url_publisher = {http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5715279} }