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

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

Namespace Prefixes

PrefixIRI
n21http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n19http://localhost/temp/predkladatel/
n17http://purl.org/net/nknouf/ns/bibtex#
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n6http://linked.opendata.cz/resource/domain/vavai/projekt/
n13http://linked.opendata.cz/ontology/domain/vavai/
n18http://linked.opendata.cz/resource/domain/vavai/zamer/
n5https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n14http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n8http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216208%3A11320%2F09%3A00207450%21RIV10-GA0-11320___/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n22http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n10http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216208%3A11320%2F09%3A00207450%21RIV10-GA0-11320___
rdf:type
skos:Concept n13:Vysledek
dcterms:description
Model checking tools based on the iterative refinement of predicate abstraction (e.g., SLAM and BLAST) often feature a specification language for expressing complex behavior rules. The source code under verification is instrumented by artificial variables and statements in order to transform the problem of checking such a rule into the problem of program location reachability. This way, the source code get bloated and additional predicates have to be discovered and tracked during the verification. We suggest that a significant performance improvement can be achieved by tracking state of the behavior rules aside from the source code instead of instrumenting them. We have implemented an extension to BLAST, which accepts a specification language (a simplified version of behavior protocols), and checks its validity without modifying the input source code. An experiment with two Linux kernel drivers confirms the performance gain using the extension. Model checking tools based on the iterative refinement of predicate abstraction (e.g., SLAM and BLAST) often feature a specification language for expressing complex behavior rules. The source code under verification is instrumented by artificial variables and statements in order to transform the problem of checking such a rule into the problem of program location reachability. This way, the source code get bloated and additional predicates have to be discovered and tracked during the verification. We suggest that a significant performance improvement can be achieved by tracking state of the behavior rules aside from the source code instead of instrumenting them. We have implemented an extension to BLAST, which accepts a specification language (a simplified version of behavior protocols), and checks its validity without modifying the input source code. An experiment with two Linux kernel drivers confirms the performance gain using the extension.
dcterms:title
Enhanced Property Specification and Verification in BLAST Enhanced Property Specification and Verification in BLAST
skos:prefLabel
Enhanced Property Specification and Verification in BLAST Enhanced Property Specification and Verification in BLAST
skos:notation
RIV/00216208:11320/09:00207450!RIV10-GA0-11320___
n4:aktivita
n7:P n7:Z
n4:aktivity
P(GA201/08/0266), Z(MSM0021620838)
n4:dodaniDat
n10:2010
n4:domaciTvurceVysledku
n9:7923384
n4:druhVysledku
n15:D
n4:duvernostUdaju
n11:S
n4:entitaPredkladatele
n8:predkladatel
n4:idSjednocenehoVysledku
313282
n4:idVysledku
RIV/00216208:11320/09:00207450
n4:jazykVysledku
n22:eng
n4:klicovaSlova
Enhanced; Property; Specification; Verification; BLAST
n4:klicoveSlovo
n14:Property n14:Enhanced n14:Verification n14:Specification n14:BLAST
n4:kontrolniKodProRIV
[5B2C9B6A4076]
n4:mistoKonaniAkce
Neuveden
n4:nazevZdroje
FASE 2009 - Fundamental Approaches to Software Engineering
n4:obor
n16:JC
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
1
n4:projekt
n6:GA201%2F08%2F0266
n4:rokUplatneniVysledku
n10:2009
n4:tvurceVysledku
Šerý, Ondřej
n4:typAkce
n21:WRD
n4:wos
000265405500032
n4:zahajeniAkce
2009-01-01+01:00
n4:zamer
n18:MSM0021620838
s:numberOfPages
14
n17:hasPublisher
Springer-Verlag
n5:isbn
978-3-642-00592-3
n19:organizacniJednotka
11320