D 2013

Compact Symbolic Execution

SLABÝ, Jiří, Jan STREJČEK and Marek TRTÍK

Basic information

Original name

Compact Symbolic Execution

Name in Czech

Kompaktní symbolická exekuce

Authors

SLABÝ, Jiří (203 Czech Republic, belonging to the institution), Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution) and Marek TRTÍK (203 Czech Republic, belonging to the institution)

Edition

Berlin Heidelberg, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, p. 193-207, 15 pp. 2013

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

Germany

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066165

Organization unit

Faculty of Informatics

ISBN

978-3-319-02443-1

ISSN

DOI

Keywords in English

symbolic execution; compact symbolic execution; testing

Tags

Tags

International impact, Reviewed
Změněno: 18/11/2013 14:45, prof. RNDr. Jan Strejček, Ph.D.

Abstract

ORIG CZ

V originále

We present a generalisation of King’s symbolic execution technique called compact symbolic execution. It proceeds in two steps. First, we analyse cyclic paths in the control flow graph of a given program, independently from the rest of the program. Our goal is to compute a so called template for each such a cyclic path. A template is a declarative parametric description of all possible program states, which may leave the analysed cyclic path after any number of iterations along it. In the second step, we execute the program symbolically with the templates in hand. The result is a compact symbolic execution tree. A compact tree always carry the same information in all its leaves as the corresponding classic symbolic execution tree. Nevertheless, a compact tree is typically substantially smaller than the corresponding classic tree. There are even programs for which compact symbolic execution trees are finite while classic symbolic execution trees are infinite.

In Czech

Prezentujeme zobecnění Kingovy symbolické exekuce nazvané kompaktní symbolická exekuce. Tato zobecněná technika pracuje ve dvou krocích. Nejdříve se analyzují cyklické cesty v grafu toku řízení daného programu nezávisle na zbytku programu. Cílem této analýzy je nalézt pro každou cyklickou cestu takzvanou šablonu. Šablona je deklarativní parametrický popis všech možných programových stavů, kterými lze opustit analyzovanou cyklickou cestu po nějakém počtu iterací podél této cesty. V druhém kroku spouštíme program symbolicky s využitím těchto šablon. Výsledkem je strom kompaktní symbolické exekuce. Tento strom nese v listech stejnou informaci jako odpovídající strom klasické symbolické exekuce. Ovšem kompaktní strom je obvykle podstatně menší než odpovídající klasický strom. Existují programy, pro které je kompaktní strom konečný, zatímco klasický strom je nekonečný.

Links

GBP202/12/G061, research and development project
Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)
Investor: Czech Science Foundation
MUNI/A/0739/2012, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0760/2012, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A