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

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

Namespace Prefixes

PrefixIRI
n9http://linked.opendata.cz/ontology/domain/vavai/cep/zivotniCyklusProjektu/
n20http://linked.opendata.cz/ontology/domain/vavai/cep/druhSouteze/
n7http://linked.opendata.cz/ontology/domain/vavai/cep/typPojektu/
dctermshttp://purl.org/dc/terms/
n2http://linked.opendata.cz/resource/domain/vavai/projekt/
n11http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/
n10http://linked.opendata.cz/resource/domain/vavai/subjekt/
n15http://linked.opendata.cz/ontology/domain/vavai/cep/kategorie/
n6http://linked.opendata.cz/ontology/domain/vavai/
n16http://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/
n14http://linked.opendata.cz/ontology/domain/vavai/cep/fazeProjektu/
n13http://linked.opendata.cz/resource/domain/vavai/projekt/GP13-37876P/
n5http://linked.opendata.cz/resource/domain/vavai/soutez/
n18http://linked.opendata.cz/ontology/domain/vavai/cep/statusZobrazovaneFaze/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
xsdhhttp://www.w3.org/2001/XMLSchema#
n4http://linked.opendata.cz/ontology/domain/vavai/cep/
n19http://linked.opendata.cz/resource/domain/vavai/aktivita/
n12http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:GP13-37876P
rdf:type
n6:Projekt
rdfs:seeAlso
http://www.isvav.cz/projectDetail.do?rowId=GP13-37876P
dcterms:description
The focus of this project is formal verification of programs with infinite state spaces. Specifically, we target programs with dynamically allocated pointer data structures and programs manipulating unbounded strings. Verification methods for both of these classes are highly desirable. The former are notoriously error-prone, hard to debug and reason about, and the latter form the main body of web applications where errors may easily lead to security vulnerabilities. We will build on methods based on symbolically encoding sets of program states using finite automata, such as regular model checking. In a connection to that, we will also investigate theory and methods facilitating practical use of finite automata in general. This especially concerns language inclusion and equivalence testing, size reduction and minimization, and decision procedures for the logics WSkS and MSO. The work on the project will include rigorous mathematical description of the developed principles and algorithms as well as their implementation and experimental evaluation. Projekt je zaměřen na formální verifikaci programů s nekonečnými stavovými prostory, zvláště pak na programy s dynamicky alokovanými ukazatelovými strukturami a programy manipulující řetězce neohraničené délky. Verifikační nástroje pro obě třídy programů jsou žádoucí. Programy s ukazateli jsou notoricky náchylné k výskytům těžko odhalitelných chyb, programy s řetězci jsou jádrem webových aplikací, kde chyba snadno vede ke kritickým bezpečnostním rizikům. Projekt staví na metodách využívajících konečné automaty jako prostředek symbolické reprezentace nekonečných množin stavů. V souvislosti s tím budeme také vyvíjet technologii umožňující využití nedeterministických konečných automatů v praxi, zejména algoritmy pro testování jazykové inkluze, minimalizaci, a rozhodovací procedury logik MSO a WSkS. Práce na projektu bude vedena rigorózními matematickými metodami a bude zahrnovat implementaci a experimentální vyhodnocení navržených technik a algoritmů.
dcterms:title
Verifikace nekonečně stavových systémů založená na konečných automatech Verification of Infinite State Systems Based on Finite Automata
skos:notation
GP13-37876P
n4:aktivita
n19:GP
n4:celkovaStatniPodpora
n13:celkovaStatniPodpora
n4:celkoveNaklady
n13:celkoveNaklady
n4:datumDodatniDoRIV
2015-02-09+01:00
n4:druhSouteze
n20:VS
n4:duvernostUdaju
n16:S
n4:fazeProjektu
n14:100993331
n4:hlavniObor
n21:IN
n4:kategorie
n15:ZV
n4:klicovaSlova
formal verification infinite state systems pointer programs string manipulating programs symbolic encoding regular model checking finite automata language inclusion minimization simulation relation
n4:partnetrHlavni
n10:orjk%3A26230
n4:pocetKoordinujicichPrijemcu
0
n4:pocetPrijemcu
1
n4:pocetSpoluPrijemcu
0
n4:pocetVysledkuRIV
5
n4:pocetZverejnenychVysledkuVRIV
5
n4:posledniUvolneniVMinulemRoce
2014-04-07+02:00
n4:prideleniPodpory
n11:13-37876P
n4:sberDatUcastniciPoslednihoRoku
n12:2015
n4:sberDatUdajeProjZameru
n12:2015
n4:soutez
n5:SGA0201300006
n4:statusZobrazovaneFaze
n18:DRRVK
n4:typPojektu
n7:P
n4:ukonceniReseni
2015-12-31+01:00
n4:zahajeniReseni
2013-02-01+01:00
n4:zivotniCyklusProjektu
n9:ZBK