Informace o publikaci

Symbolic Computation via Program Transformation

Autoři

LAUKO Henrich ROČKAI Petr BARNAT Jiří

Rok publikování 2018
Druh Článek ve sborníku
Konference Theoretical Aspects of Computing – ICTAC 2018
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www 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
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info