Symbolic Computation via Program Transformation
Abstract
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.
The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover, using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend
- Authors: Henrich Lauko, Jiří Barnát, and Petr Ročkai
- Conference: Theoretical Aspects of Computing – ICTAC 2018
- Paper details: Page with PDF
- Reference to the local database of the institution
- ResearchGate
Citation
LAUKO, Henrich, Petr ROČKAI and Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018. p. 313-332, 20 pp. ISBN 978-3-030-02507-6. doi:10.1007/978-3-030-02508-3_17.