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
• 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

• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
• Abstrakce a jiné techniky v semi-symbolické verifikaci programů
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18