Informace o publikaci
Symbolic Computation via Program Transformation
| Autoři | |
|---|---|
| Rok publikování | 2018 |
| Druh | Článek ve sborníku |
| Konference | Theoretical Aspects of Computing – ICTAC 2018 |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | https://link.springer.com/chapter/10.1007/978-3-030-02508-3_17 |
| Doi | https://doi.org/10.1007/978-3-030-02508-3_17 |
| Klíčová slova | Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++ |
| Popis | 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. |
| Související projekty: |