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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F07%3A00020381%21RIV10-GA0-14330___
rdf:type
skos:Concept n5:Vysledek
dcterms:description
With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements.
dcterms:title
Tutorial: Parallel Model Checking Tutorial: Parallel Model Checking
skos:prefLabel
Tutorial: Parallel Model Checking Tutorial: Parallel Model Checking
skos:notation
RIV/00216224:14330/07:00020381!RIV10-GA0-14330___
n3:aktivita
n9:Z n9:P
n3:aktivity
P(1M0545), P(GA201/06/1338), Z(MSM0021622419)
n3:dodaniDat
n16:2010
n3:domaciTvurceVysledku
n13:5692792 n13:6500773
n3:druhVysledku
n18:D
n3:duvernostUdaju
n8:S
n3:entitaPredkladatele
n10:predkladatel
n3:idSjednocenehoVysledku
456020
n3:idVysledku
RIV/00216224:14330/07:00020381
n3:jazykVysledku
n19:eng
n3:klicovaSlova
LTL Parallel Model Checking
n3:klicoveSlovo
n15:LTL%20Parallel%20Model%20Checking
n3:kontrolniKodProRIV
[66E09069B18D]
n3:mistoKonaniAkce
Berlin, Germany
n3:mistoVydani
Berlin, Heidelberg
n3:nazevZdroje
Model Checking Software
n3:obor
n22:IN
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
2
n3:projekt
n11:GA201%2F06%2F1338 n11:1M0545
n3:rokUplatneniVysledku
n16:2007
n3:tvurceVysledku
Brim, Luboš Barnat, Jiří
n3:typAkce
n17:WRD
n3:wos
000247906900002
n3:zahajeniAkce
2007-01-01+01:00
n3:zamer
n21:MSM0021622419
s:issn
0302-9743
s:numberOfPages
2
n20:hasPublisher
Springer-Verlag
n6:isbn
978-3-540-73369-0
n12:organizacniJednotka
14330