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

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

Namespace Prefixes

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

Statements

Subject Item
n2:GA14-11384S
rdf:type
n16:Projekt
rdfs:seeAlso
http://www.isvav.cz/projectDetail.do?rowId=GA14-11384S
dcterms:description
Projekt směřuje do oblasti formální verifikace nekonečně stavových softwarových systémů. Konkrétně se soustředí na zvýšení automatizace, škálovatelnosti a obecnosti současných metod formální verifikace programů s neomezenými datovými strukturami, jako jsou ukazatelové struktury a kolekce, obsahujícími data z případně neomezených domén a/nebo používající neomezený či parametrický paralelismus. V případě paralelních programů bude kladen důraz zejména na programy používající moderní synchronizační prostředky, jako jsou bezzámkové struktury či transakční paměti. S cílem umožnit verifikaci takových programů se projekt zaměřuje na rozvoj stávajících a návrh nových metod symbolické verifikace založených na využití automatů a logik. Při řešení projektu budou řešitelé konkrétně vycházet ze svých hlubokých a vzájemně se doplňujících zkušeností s abstraktním regulárním model checkingem, automaty nad stromy a lesy, separační logikou a symbolickými grafy paměti, predikátovou abstrakcí pro data a kolekce a vláknově modulární verifikací paralelních programů. The project targets formal verification of infinite-state software systems. In particular, it aims at improving the degree of automation, scalability, and generality of the current approaches to formal verification of programs handling unbounded data structures, such as collections or dynamic linked data structures based on pointers, possibly storing data from unbounded domains, and/or using unbounded or parametric concurrency. As for concurrent programs, the stress will be on programs using modern synchronization means such as lockless data structures or transactional memories. To handle such programs, the project focuses on extending the current and developing new symbolic verification approaches based on automata and/or logics. When working on the project, members of the project teams will build on their deep and mutually complementary expertise with abstract regular model checking, tree and forest automata, separation logic and symbolic memory graphs, predicate abstraction over primitive data and collections, and thread modular verification of concurrent programs.
dcterms:title
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
skos:notation
GA14-11384S
n3:aktivita
n13:GA
n3:celkovaStatniPodpora
n4:celkovaStatniPodpora
n3:celkoveNaklady
n4:celkoveNaklady
n3:datumDodatniDoRIV
2015-04-23+02:00
n3:druhSouteze
n19:VS
n3:duvernostUdaju
n5:S
n3:fazeProjektu
n8:100791972
n3:hlavniObor
n7:JC
n3:kategorie
n9:ZV
n3:klicovaSlova
formal verification, symbolic verification, infinite-state systems, theory of automata, logic, dynamic linked data structures, collections, parametric systems, concurrency
n3:partnetrHlavni
n11:orjk%3A26230
n3:pocetKoordinujicichPrijemcu
0
n3:pocetPrijemcu
1
n3:pocetSpoluPrijemcu
1
n3:pocetVysledkuRIV
14
n3:pocetZverejnenychVysledkuVRIV
14
n3:posledniUvolneniVMinulemRoce
2014-04-18+02:00
n3:prideleniPodpory
n12:14-11384S
n3:sberDatUcastniciPoslednihoRoku
n10:2015
n3:sberDatUdajeProjZameru
n10:2015
n3:soutez
n14:SGA0201400001
n3:statusZobrazovaneFaze
n21:DRRVB
n3:typPojektu
n17:P
n3:ukonceniReseni
2016-12-31+01:00
n3:zahajeniReseni
2014-01-01+01:00
n3:zivotniCyklusProjektu
n20:ZB
n3:klicoveSlovo
theory of automata symbolic verification infinite-state systems collections parametric systems logic dynamic linked data structures formal verification