Symbolic Computation via Program Transformation

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
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:

You are running an old browser version. We recommend updating your browser to its latest version.