Compact Symbolic Execution
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066165" target="_blank" >RIV/00216224:14330/13:00066165 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_15" target="_blank" >http://dx.doi.org/10.1007/978-3-319-02444-8_15</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-02444-8_15" target="_blank" >10.1007/978-3-319-02444-8_15</a>
Alternative languages
Result language
angličtina
Original language name
Compact Symbolic Execution
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
ISBN
9783319024431
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
193-207
Publisher name
Springer
Place of publication
Berlin Heidelberg
Event location
Hanoi, Vietnam
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—