Publication details

Symbolic Computation via Program Transformation

Authors

LAUKO Henrich ROČKAI Petr BARNAT Jiří

Year of publication 2018
Type Article in Proceedings
Conference Theoretical Aspects of Computing – ICTAC 2018
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007/978-3-030-02508-3_17
Doi http://dx.doi.org/10.1007/978-3-030-02508-3_17
Keywords Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Description Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs a semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them; therefore, the program can be processed by a tool without support for symbolic manipulation.
Related projects: