Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik

Poskytovatel

Grantová agentura České republiky

Program

Postdoktorandské granty

Veřejná soutěž

Postdoktorandské granty 8 (SGA02008GA1PD)

Hlavní účastníci

—

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

201/08/P375

Název projektu anglicky

Formal verification: algorithms, properties of modelling formalisms and temporal logics

Anotace anglicky

Quality assurance processes based mainly on humans are not suitable for development of current extensive hardware and software systems. Application of automatic verification tools is a promising solution. Research in the area of automatic formal verification is the aim of the proposed project. More precisely, the proposer intends to focus on the following three areas. Properties of temporal logics and aplication of these properties to development of new or improvement of the current verificationalgorithms properties of formalisms for modeling infinite-state systems - their expressive power and decidability of basic verification problems for the corresponding classes of infinite-state systems progressive directions in software verifications - inparticular verification of properties related to dynamic memory allocation and applications of verification techiques to common programming languages. The output of this research project will be papers in international journals and papers at

Kategorie VaV

ZV - Základní výzkum

CEP - hlavní obor

IN - Informatika

CEP - vedlejší obor

—

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)

Hodnocení poskytovatelem

U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)

Zhodnocení výsledků projektu

Cílem projektu bylo dosažení výsledků ve třech oblastech: vlastnosti temporálních logik, vlastnosti nekonečně-stavových systémů a progresivní směry ve verifikaci softwaru. V první oblasti jsme nejprve dokázali, že fragment LTL obsahující modality eventu?

Zahájení řešení

1. 1. 2008

Ukončení řešení

31. 12. 2010

Poslední stav řešení

U - Ukončený projekt

Poslední uvolnění podpory

16. 4. 2010

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

CEP11-GA0-GP-U/04:3

Datum dodání záznamu

20. 3. 2015

Celkové uznané náklady

435 tis. Kč

Výše podpory ze státního rozpočtu

435 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč