Symbolic Computation via Program Transformation

D 2018

Symbolic Computation via Program Transformation

LAUKO, Henrich, Petr ROČKAI a Jiří BARNAT

Základní údaje

Originální název

Symbolic Computation via Program Transformation

Autoři

LAUKO, Henrich (703 Slovensko, domácí), Petr ROČKAI (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí)

Vydání

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

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00101301

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-02507-6

ISSN

DOI

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

UT WoS

000612998900017

Klíčová slova anglicky

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

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 20. 9. 2022 11:14, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

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

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

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

LAUKO, Henrich, Petr ROČKAI a Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018, s. 313-332. ISBN 978-3-030-02507-6. Dostupné z: 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  - JOUR
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 a Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. \textit{Theoretical Aspects of Computing – ICTAC 2018}. Cham (Switzerland): Springer, 2018, s.~313-332. ISBN~978-3-030-02507-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02508-3\_{}17.

Podrobný výpis o publikaci