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

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

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

Keywords in English

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

Tags

core_B, firank_B

Tags

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

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
Displayed: 8/11/2024 10:49