Model checking paralelního software s využitím automatické dedukce object ownership vzorů

Poskytovatel

Grantová agentura České republiky

Program

Postdoktorandské granty

Veřejná soutěž

Postdoktorandské granty 12 (SGA02012GA1PD)

Hlavní účastníci

—

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

P202-12-P180

Název projektu anglicky

Model checking concurrent software using automated deduction of object ownership patterns

Anotace anglicky

Due to state space explosion, verification of concurrent software using model checking is a notoriously hard task. Correctness of concurrent software relies on adherence to certain synchronization rules established by the developers but not explicitly expressed in the program code. Such rules often describe object ownership which relates objects with rules of how to access them in the concurrent environment (e.g., a data structure is owned by a lock). On the one hand, this information might extremely useful for verification of concurrent software. On the other hand, except in very specific cases, it is unrealistic to expect developers to provide it in a form amenable to automated reasoning. In this project, we will design a method for automated deduction of object ownership patterns. Further, we will extend current on-the-fly partial-order-reduction techniques to use this information for more efficient pruning of the search space during the subsequent model checking. We will also develop a prototype implementation.

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

O - Nesplněno zadání, smlouva však byla dodržena

Zhodnocení výsledků projektu

Tento tříletý projekt skončil po prvním roce z důvodů ukončení pracovního poměru řešitele. Šlo o rozšíření technik verifikace vícevláknového software. Článek vedoucí k navrhovanému výzkumu řešitel publikoval se zahraničními spoluautory na prestižní konf?

Zahájení řešení

1. 1. 2012

Ukončení řešení

31. 12. 2013

Poslední stav řešení

S - Zastavený (předčasně ukončený) víceletý projekt

Poslední uvolnění podpory

30. 3. 2013

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

CEP15-GA0-GP-U/02:2

Datum dodání záznamu

6. 5. 2016

Celkové uznané náklady

672 tis. Kč

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

672 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

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

0 tis. Kč