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. doi:10.1007/978-3-030-02508-3_17.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Symbolic Computation via Program Transformation
Autoři LAUKO, Henrich (703 Slovensko), Petr ROČKAI (703 Slovensko) 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
Originální 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"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-02508-3_17
Klíčová slova anglicky Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 30. 4. 2019 07:35.
Anotace
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 VaVNázev: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/0854/2017, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1038/2017, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 9. 12. 2021 14:12