Symbolic Computation via Program Transformation

D 2018

Symbolic Computation via Program Transformation

LAUKO, Henrich; Petr ROČKAI and Jiří BARNAT

Basic information

Original name

Symbolic Computation via Program Transformation

Authors

LAUKO, Henrich (703 Slovakia, belonging to the institution); Petr ROČKAI (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution)

Edition

Cham (Switzerland), Theoretical Aspects of Computing – ICTAC 2018, p. 313-332, 20 pp. 2018

Publisher

Springer

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

is not subject to a state or trade secret

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/18:00101301

Organization unit

Faculty of Informatics

ISBN

978-3-030-02507-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-02508-3_17

UT WoS

000612998900017

EID Scopus

2-s2.0-85055428224

Keywords in English

Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++

Abstract

V originále

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.

Links

GA18-02177S, research and development project

Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation

MUNI/A/0854/2017, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masaryk University, Category A

MUNI/A/1038/2017, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18

Investor: Masaryk University, Category A

Cite

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. ISBN 978-3-030-02507-6. Available from: https://dx.doi.org/10.1007/978-3-030-02508-3_17.

@inproceedings{1459216,
   author = {Lauko, Henrich and Ročkai, Petr and Barnat, Jiří},
   address = {Cham (Switzerland)},
   booktitle = {Theoretical Aspects of Computing – ICTAC 2018},
   doi = {http://dx.doi.org/10.1007/978-3-030-02508-3_17},
   editor = {Bernd Fischer, Tarmo Uustalu},
   keywords = {Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-02507-6},
   pages = {313-332},
   publisher = {Springer},
   title = {Symbolic Computation via Program Transformation},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-02508-3_17},
   year = {2018}
}

TY  - CONF
ID  - 1459216
AU  - Lauko, Henrich - Ročkai, Petr - Barnat, Jiří
PY  - 2018
TI  - Symbolic Computation via Program Transformation
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030025076
KW  - Symbolic Computation
KW  - Abstraction
KW  - DIVINE
KW  - LLVM
KW  - Transformation
KW  - Verification
KW  - Model Checking
KW  - C
KW  - C++
UR  - https://link.springer.com/chapter/10.1007/978-3-030-02508-3_17
N2  - 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.
ER  -

LAUKO, Henrich; Petr ROČKAI and Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. \textit{Theoretical Aspects of Computing – ICTAC 2018}. Cham (Switzerland): Springer, 2018, p.~313-332. ISBN~978-3-030-02507-6. Available from: https://dx.doi.org/10.1007/978-3-030-02508-3\_{}17.

Přehled o publikaci