This HTML5 document contains 47 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n20http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n15http://localhost/temp/predkladatel/
n9http://purl.org/net/nknouf/ns/bibtex#
n18http://linked.opendata.cz/resource/domain/vavai/projekt/
n10http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n23http://linked.opendata.cz/resource/domain/vavai/subjekt/
n21http://linked.opendata.cz/ontology/domain/vavai/
n14https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n16http://bibframe.org/vocab/
n4http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F13%3A00066165%21RIV14-MSM-14330___/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n8http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n22http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n19http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F13%3A00066165%21RIV14-MSM-14330___
rdf:type
skos:Concept n21:Vysledek
dcterms: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. 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.
dcterms:title
Compact Symbolic Execution Compact Symbolic Execution
skos:prefLabel
Compact Symbolic Execution Compact Symbolic Execution
skos:notation
RIV/00216224:14330/13:00066165!RIV14-MSM-14330___
n21:predkladatel
n23:orjk%3A14330
n3:aktivita
n11:S n11:P
n3:aktivity
P(GBP202/12/G061), S
n3:dodaniDat
n19:2014
n3:domaciTvurceVysledku
n10:6545270 n10:3978915 n10:9937056
n3:druhVysledku
n6:D
n3:duvernostUdaju
n17:S
n3:entitaPredkladatele
n4:predkladatel
n3:idSjednocenehoVysledku
66055
n3:idVysledku
RIV/00216224:14330/13:00066165
n3:jazykVysledku
n22:eng
n3:klicovaSlova
symbolic execution; compact symbolic execution; testing
n3:klicoveSlovo
n8:compact%20symbolic%20execution n8:testing n8:symbolic%20execution
n3:kontrolniKodProRIV
[B96DF5028FCD]
n3:mistoKonaniAkce
Hanoi, Vietnam
n3:mistoVydani
Berlin Heidelberg
n3:nazevZdroje
11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
n3:obor
n13:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n18:GBP202%2F12%2FG061
n3:rokUplatneniVysledku
n19:2013
n3:tvurceVysledku
Slabý, Jiří Strejček, Jan Trtík, Marek
n3:typAkce
n20:WRD
n3:zahajeniAkce
2013-01-01+01:00
s:issn
0302-9743
s:numberOfPages
15
n16:doi
10.1007/978-3-319-02444-8_15
n9:hasPublisher
Springer-Verlag
n14:isbn
9783319024431
n15:organizacniJednotka
14330