About: Verifikace nekonečně stavových systémů založená na konečných automatech

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Verifikace nekonečně stavových systémů založená na konečných automatech Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Projekt, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	http://linked.opendata.cz/ontology/domain/vavai/Projekt
rdfs:seeAlso	http://www.isvav.cz/projectDetail.do?rowId=GP13-37876P
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. (en) 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ů.
Title	Verifikace nekonečně stavových systémů založená na konečných automatech Verification of Infinite State Systems Based on Finite Automata (en)
skos:notation	GP13-37876P
http://linked.open...avai/cep/aktivita	Post-graduate (doctorate) grants
http://linked.open...kovaStatniPodpora	http://linked.opendata.cz/resource/domain/vavai/projekt/GP13-37876P/celkovaStatniPodpora
http://linked.open...ep/celkoveNaklady	http://linked.opendata.cz/resource/domain/vavai/projekt/GP13-37876P/celkoveNaklady
http://linked.open...datumDodatniDoRIV	2015-02-09 (xsd:date)
http://linked.open...i/cep/druhSouteze	VS - Veřejná soutěž ve výzkumu a vývoji
http://linked.open...ep/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open.../cep/fazeProjektu	100993331
http://linked.open...ai/cep/hlavniObor	IN - Informatika
http://linked.open...vai/cep/kategorie	ZV - Základní výzkum
http://linked.open.../cep/klicovaSlova	formal verification infinite state systems pointer programs string manipulating programs symbolic encoding regular model checking finite automata language inclusion minimization simulation relation (en)
http://linked.open...ep/partnetrHlavni	Fakulta informačních technologií
http://linked.open...inujicichPrijemcu	0 (xsd:int)
http://linked.open...cep/pocetPrijemcu	1 (xsd:int)
http://linked.open...ocetSpoluPrijemcu	0 (xsd:int)
http://linked.open.../pocetVysledkuRIV	5 (xsd:int)
http://linked.open...enychVysledkuVRIV	5 (xsd:int)
http://linked.open...lneniVMinulemRoce	2014-04-07 (xsd:date)
http://linked.open.../prideleniPodpory	http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/13-37876P
http://linked.open...iciPoslednihoRoku	2015
http://linked.open...atUdajeProjZameru	2015
http://linked.open.../vavai/cep/soutez	SGA0201300006
http://linked.open...usZobrazovaneFaze	DRRVK
http://linked.open...ai/cep/typPojektu	P - Projekt výzkumu a vývoje financovaný ze státního rozpočtu
http://linked.open...ep/ukonceniReseni	2015-12-31 (xsd:date)
http://linked.open...ep/zahajeniReseni	2013-02-01 (xsd:date)
http://linked.open...tniCyklusProjektu	ZBK
is http://linked.open...vavai/cep/projekt of	http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GP13-37876P/2013/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GP13-37876P/2014/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GP13-37876P/2015/orjk%3A26230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software