Symbolic Computation via Program Transformation
| Authors | |
|---|---|
| Year of publication | 2018 |
| Type | Article in Proceedings |
| Conference | Theoretical Aspects of Computing – ICTAC 2018 |
| MU Faculty or unit | |
| 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: |