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
n13http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
n14http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F08%3APU70924%21RIV10-MSM-26230___/
dctermshttp://purl.org/dc/terms/
n18http://localhost/temp/predkladatel/
n16http://purl.org/net/nknouf/ns/bibtex#
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n17http://linked.opendata.cz/ontology/domain/vavai/
n5http://linked.opendata.cz/resource/domain/vavai/zamer/
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/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n8http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n10http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n12http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F08%3APU70924%21RIV10-MSM-26230___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
The paper presents a new approach to formal verification of generic (i.e. parametrised) hardware designs specified in VHDL. The proposed approach is based on a translation of such designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. We have implemented the proposed translation. Using one of the state-of-the-art tools for verification of counter automata, we were then able to verify several non-trivial properties of parametrised VHDL components, including a real-life one. The paper presents a new approach to formal verification of generic (i.e. parametrised) hardware designs specified in VHDL. The proposed approach is based on a translation of such designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. We have implemented the proposed translation. Using one of the state-of-the-art tools for verification of counter automata, we were then able to verify several non-trivial properties of parametrised VHDL components, including a real-life one.
dcterms:title
Verifying Parametrised Hardware Designs Via Counter Automata Verifying Parametrised Hardware Designs Via Counter Automata
skos:prefLabel
Verifying Parametrised Hardware Designs Via Counter Automata Verifying Parametrised Hardware Designs Via Counter Automata
skos:notation
RIV/00216305:26230/08:PU70924!RIV10-MSM-26230___
n3:aktivita
n6:Z
n3:aktivity
Z(MSM0021630528), Z(MSM6383917201)
n3:dodaniDat
n12:2010
n3:domaciTvurceVysledku
n9:9761985 n9:1458841
n3:druhVysledku
n15:D
n3:duvernostUdaju
n10:S
n3:entitaPredkladatele
n14:predkladatel
n3:idSjednocenehoVysledku
402554
n3:idVysledku
RIV/00216305:26230/08:PU70924
n3:jazykVysledku
n19:eng
n3:klicovaSlova
formal verification, hardware design, counter automaton, VHDL<br>
n3:klicoveSlovo
n8:hardware%20design n8:formal%20verification n8:VHDL%3Cbr%3E n8:counter%20automaton
n3:kontrolniKodProRIV
[DF433F1CC75E]
n3:mistoKonaniAkce
IBM Haifa Labs
n3:mistoVydani
Heidelberg
n3:nazevZdroje
Hardware and Software, Verification and Testing
n3:obor
n4:JC
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
2
n3:rokUplatneniVysledku
n12:2008
n3:tvurceVysledku
Vojnar, Tomáš Smrčka, Aleš
n3:typAkce
n13:WRD
n3:zahajeniAkce
2007-10-23+02:00
n3:zamer
n5:MSM0021630528 n5:MSM6383917201
s:issn
0302-9743
s:numberOfPages
18
n16:hasPublisher
Springer-Verlag
n18:organizacniJednotka
26230