Automaty a logiky v symbolické verifikaci software.

Název projektu anglicky
Automata and Logic for Symbolic Verification of Software
Anotace anglicky
The scientific goal of the proposed project is to significantly advance the state of the art in the area of symbolic logic-based and automata-based verification methods for infinite-state software, namely to increase the scalability of these approaches and to broaden the area of their applicability. To achieve this goal we plan to further improve the various individual logic-based as well as automata-based techniques, but also invest a significant amount of research into approaches combining advantagesof both automata as well as logics. In the research, we will in particular concentrate on verification of programs with unbounded integers, (parametrised-size) arrays, and complex dynamic linked data structures.

Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
JC - Počítačový hardware a software
CEP - vedlejší obor
IN - Informatika
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)<br>20206 - Computer hardware and architecture

Hodnocení poskytovatelem
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Zhodnocení výsledků projektu
Projekt se zabýval základním výzkumem v oblasti verifikace nekonečně stavových systémů. Výsledkem je nová technika pro verifikaci práce s dynamickou pamětí a nové techniky pro ověřování vlastností čítačových automatů.

Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP12-MSM-ME-U/01:1
Datum dodání záznamu
12. 7. 2012

Podobné projekty(10)