Verification of Infinite State Systems Based on Finite Automata
Public support
Provider
Czech Science Foundation
Programme
Post-graduate (doctorate) grants
Call for proposals
Postdoktorandské granty 14 (SGA0201300006)
Main participants
—
Contest type
VS - Public tender
Contract ID
13-37876P
Alternative language
Project name in Czech
Verifikace nekonečně stavových systémů založená na konečných automatech
Annotation in Czech
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ů.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
IN - Informatics
CEP - secondary branch
—
CEP - another secondary branch
—
OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
Within an international cooperation, the project has shifted the state-of-the-art in the area of system verification, with several results presented at the top venues (like, e.g., conferences CAV and TACAS), which has included developing software tools for program verification.
Solution timeline
Realization period - beginning
Feb 1, 2013
Realization period - end
Dec 31, 2015
Project status
U - Finished project
Latest support payment
Apr 10, 2015
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP16-GA0-GP-U/01:1
Data delivery date
May 6, 2016
Finance
Total approved costs
2,289 thou. CZK
Public financial support
2,289 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK