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

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

Namespace Prefixes

PrefixIRI
n11http://linked.opendata.cz/ontology/domain/vavai/cep/druhSouteze/
n16http://linked.opendata.cz/ontology/domain/vavai/cep/typPojektu/
n4http://linked.opendata.cz/ontology/domain/vavai/cep/zivotniCyklusProjektu/
n17http://linked.opendata.cz/ontology/domain/vavai/cep/hodnoceniProjektu/
dctermshttp://purl.org/dc/terms/
n2http://linked.opendata.cz/resource/domain/vavai/projekt/
n8http://linked.opendata.cz/resource/domain/vavai/subjekt/
n7http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/
n15http://linked.opendata.cz/ontology/domain/vavai/
n14http://linked.opendata.cz/ontology/domain/vavai/cep/kategorie/
n18http://linked.opendata.cz/ontology/domain/vavai/cep/duvernostUdaju/
rdfshttp://www.w3.org/2000/01/rdf-schema#
skoshttp://www.w3.org/2004/02/skos/core#
n21http://linked.opendata.cz/ontology/domain/vavai/cep/obor/
n19http://linked.opendata.cz/ontology/domain/vavai/cep/fazeProjektu/
n5http://linked.opendata.cz/resource/domain/vavai/soutez/
n9http://linked.opendata.cz/ontology/domain/vavai/cep/statusZobrazovaneFaze/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n12http://linked.opendata.cz/resource/domain/vavai/projekt/GAP103%2F10%2F0306/
xsdhhttp://www.w3.org/2001/XMLSchema#
n3http://linked.opendata.cz/ontology/domain/vavai/cep/
n13http://reference.data.gov.uk/id/gregorian-year/
n10http://linked.opendata.cz/resource/domain/vavai/aktivita/

Statements

Subject Item
n2:GAP103%2F10%2F0306
rdf:type
n15:Projekt
rdfs:seeAlso
http://www.isvav.cz/projectDetail.do?rowId=GAP103/10/0306
dcterms:description
Automatizovaná verifikace programů je v současnosti s ohledem na rostoucí dopad počítačem řízených systémů na naše životy a výraznou potřebu minimalizovat počet chyb v těchto systémech velmi aktuálním výzkumným tématem. Projekt se konkrétně zaměřuje na verifikaci programů s pokročilými rysy paralelismu a neomezenosti, které patří k obzvláště problematickým aspektům software, se kterými se musí automatická verifikace vyrovnávat. V prvním případě se projekt soustřeďuje zejména na metody verifikace programů určených pro moderní vícejádrové procesory. V druhém případě se jedná o verifikaci programů pracujících s různými neomezenými datovými strukturami, zejména pak poli (o parametrické velikosti) a složitými dynamickými strukturami založenými na ukazatelích (jako jsou seznamy či stromy). Projekt zahrnuje výzkum metod dynamické i statické verifikace, včetně model checkingu, a také jejích vhodných kombinací. Pro práci s programy s nekonečnými stavovými prostory se výzkum v projektu zaměřuje na metody efektivní symbolické verifikace založené na použití automatů a logik. Automated verification of programs is currently a very hot issue due to the rising influence of computer-controlled systems on our lives and the recognised need to minimise the number of errors in them. The project, in particular, considers verification of programs with advanced features of concurrency and unboundedness, which both belong among especially problematic features to be dealt with in automated verification. In the former case, the project pays a special attention to verification of applications intended to run on the current multi-core processors. In the latter case, verification of programs manipulating different unbounded structures, notably (parameterised-size) arrays and complex dynamic linked data structures (such as lists or trees), is considered. The project contains research on methods of dynamic as well as static verification, including model checking, and possibly their suitable combinations. For handling infinite-state programs, efficient symbolic verification methods based on automata and logics are the primary target of the research in the project.
dcterms:title
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti
skos:notation
GAP103/10/0306
n3:aktivita
n10:GA
n3:celkovaStatniPodpora
n12:celkovaStatniPodpora
n3:celkoveNaklady
n12:celkoveNaklady
n3:datumDodatniDoRIV
2014-07-01+02:00
n3:druhSouteze
n11:VS
n3:duvernostUdaju
n18:S
n3:fazeProjektu
n19:100267384
n3:hlavniObor
n21:JC
n3:hodnoceniProjektu
n17:U
n3:kategorie
n14:ZV
n3:klicovaSlova
verification engineering automated verification of programs static and dynamic analysis formal verification model checking concurrency multicore processors infinite-state programs dynamic data structures
n3:partnetrHlavni
n8:orjk%3A26230
n3:pocetKoordinujicichPrijemcu
0
n3:pocetPrijemcu
1
n3:pocetSpoluPrijemcu
0
n3:pocetVysledkuRIV
63
n3:pocetZverejnenychVysledkuVRIV
63
n3:posledniUvolneniVMinulemRoce
2013-06-12+02:00
n3:prideleniPodpory
n7:P103-10-0306
n3:sberDatUcastniciPoslednihoRoku
n13:2013
n3:sberDatUdajeProjZameru
n13:2014
n3:soutez
n5:SGA02010GA-ST
n3:statusZobrazovaneFaze
n9:DUU
n3:typPojektu
n16:P
n3:ukonceniReseni
2013-12-31+01:00
n3:vedlejsiObor
n21:IN
n3:zahajeniReseni
2010-01-01+01:00
n3:zhodnoceni+vysledku+projektu+dodavatelem
The project has brought internationally recognized results in the formal verification of programs with various sources of unboundedness and of concurrent programs. These were high quality publications in journals (7) and at international conferences (31), as well as publicly available software tools for experiments in program verification. Three conference papers received a best paper award. Projekt přinesl mezinárodně významné výsledky ve formální verifikaci programů s různými zdroji neomezenosti a paralelních programů. Těmi byly vysoce kvalitní publikace v časopisech (7) a na mezinárodních konferencích (31), jakož i veřejně dostupné softwarové nástroje pro experimenty v oblasti verifikace programů. Tři konferenční články získaly ocenění za nejlepší článek.
n3:zivotniCyklusProjektu
n4:ZBBKU