Abstract State Machines (ASMs) are a well-known state based formal method to describe systems at a very high level and can be executed either through a concrete or symbolic interpretation. By symbolically executing an ASM specification, certain properties can be checked by transforming the described ASM into a suitable input for model checkers or Automated Theorem Provers (ATPs). Due to the rather fast increasing state space, model checking and ATP solutions can lead to inefficient implementations of symbolic execution. More efficient state space and execution performance can be achieved by using a concolic execution approach. In this paper, we describe an improved concolic execution implementation for the Corinthian Abstract State Machine (CASM) language. We outline the transformation of a symbolically executed ASM specification to a single Thousands of Problems for Theorem Provers (TPTP) format. Furthermore, we introduce a compiler analysis to promote concrete ASM functions into symbolic ones in order to obtain symbolic consistency.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{PaulweberMZ21,
author = {Philipp Paulweber and
Jakob Moosbrugger and
Uwe Zdun},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry},
title = {About the Concolic Execution and Symbolic {ASM} Function Promotion
in {CASM}},
booktitle = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
2021, Ulm, Germany, June 9-11, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12709},
pages = {112--117},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-77543-8\_9},
doi = {10.1007/978-3-030-77543-8\_9},
timestamp = {Sat, 09 Apr 2022 12:45:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/PaulweberMZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}