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. doi:10.1007/978-3-030-02508-3_17.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Symbolic Computation via Program Transformation
Authors LAUKO, Henrich (703 Slovakia), Petr ROČKAI (703 Slovakia) 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
Original 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"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-02508-3_17
Keywords in English Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 30/4/2019 07:35.
Abstract
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 projectName: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Czech Science Foundation, Standard Projects
MUNI/A/0854/2017, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/1038/2017, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 21/1/2022 13:12