This HTML5 document contains 49 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/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F12%3A00057431%21RIV13-GA0-14330___/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n15http://purl.org/net/nknouf/ns/bibtex#
n5http://localhost/temp/predkladatel/
n12http://linked.opendata.cz/resource/domain/vavai/projekt/
n10http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n19http://linked.opendata.cz/resource/domain/vavai/subjekt/
n17http://linked.opendata.cz/ontology/domain/vavai/
n23https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n21http://bibframe.org/vocab/
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/
n22http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n9http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n16http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F12%3A00057431%21RIV13-GA0-14330___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
We introduce a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positives from an output of another bug-finding tool. We provide several examples demonstrating the practical applicability of our technique. We introduce a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positives from an output of another bug-finding tool. We provide several examples demonstrating the practical applicability of our technique.
dcterms:title
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
skos:prefLabel
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
skos:notation
RIV/00216224:14330/12:00057431!RIV13-GA0-14330___
n17:predkladatel
n19:orjk%3A14330
n3:aktivita
n4:S n4:P
n3:aktivity
P(GBP202/12/G061), S
n3:dodaniDat
n16:2013
n3:domaciTvurceVysledku
n10:3978915 n10:9937056 n10:6545270
n3:druhVysledku
n13:D
n3:duvernostUdaju
n22:S
n3:entitaPredkladatele
n20:predkladatel
n3:idSjednocenehoVysledku
126923
n3:idVysledku
RIV/00216224:14330/12:00057431
n3:jazykVysledku
n9:eng
n3:klicovaSlova
Bug finding; Symbolic execution; Program slicing; FSM property specification; Code instrumentation
n3:klicoveSlovo
n8:Code%20instrumentation n8:Bug%20finding n8:FSM%20property%20specification n8:Symbolic%20execution n8:Program%20slicing
n3:kontrolniKodProRIV
[FBAC2A1874D3]
n3:mistoKonaniAkce
Paris, France
n3:mistoVydani
Berlin, Heidelberg
n3:nazevZdroje
Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012
n3:obor
n14:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n12:GBP202%2F12%2FG061
n3:rokUplatneniVysledku
n16:2012
n3:tvurceVysledku
Slabý, Jiří Trtík, Marek Strejček, Jan
n3:typAkce
n7:WRD
n3:zahajeniAkce
2012-01-01+01:00
s:issn
0302-9743
s:numberOfPages
15
n21:doi
10.1007/978-3-642-32469-7_14
n15:hasPublisher
Springer-Verlag
n23:isbn
9783642324680
n5:organizacniJednotka
14330