Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

Analýza korektnosti vícevláknových programů v C a C++

Veřejná podpora

  • Poskytovatel

    Grantová agentura České republiky

  • Program

    Standardní projekty

  • Veřejná soutěž

    Standardní projekty 19 (SGA0201500001)

  • Hlavní účastníci

    Masarykova univerzita / Fakulta informatiky

  • Druh soutěže

    VS - Veřejná soutěž

  • Číslo smlouvy

    15-08772S

Alternativní jazyk

  • Název projektu anglicky

    Correctness Analysis of C and C++ Programs with Threads

  • Anotace anglicky

    The goal of this project is to research and develop new algorithms and data structures to support model checking of multi-threaded programs written in the C and C++ programming languages. The particular goals of the project include the development of new techniques for automated program abstraction by means of program transformation, techniques for efficient combination of explicit and symbolic approaches to model checking. We will also seek additional techniques for reducing memory requirements of formal verification tools, model checkers in particular. The newly developed data structures and algorithms will be implemented and evaluated within the context of the parallel LTL model checker DIVINE. Our intent is to push the tractability frontier in the area of multi-threaded C and C++ programs, taking advantage of contemporary computational platforms such as multi-core workstations or high-performance clusters.

Vědní obory

  • 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í dokončeného projektu

  • Hodnocení poskytovatelem

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

  • Zhodnocení výsledků projektu

    Projekt přináší nové výsledky v oblasti automatizované formální verifikace metodou ověřování modelu publikované ve 12 konferenčních a 3 časopiseckých (Jimp) článcích přijatelné kvality. Navržené metody byly implementovány v rámci nástroje DIVINE a experimentálně zanalyzovány. Studenti různých studijních programů byli do projektu aktivně zapojováni. Finance byly čerpány účelně.

Termíny řešení

  • Zahájení řešení

    1. 1. 2015

  • Ukončení řešení

    31. 12. 2017

  • Poslední stav řešení

    U - Ukončený projekt

  • Poslední uvolnění podpory

    5. 4. 2017

Dodání dat do CEP

  • 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

    CEP18-GA0-GA-U/02:1

  • Datum dodání záznamu

    4. 5. 2018

Finance

  • Celkové uznané náklady

    4 998 tis. Kč

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

    4 998 tis. Kč

  • Ostatní veřejné zdroje financování

    0 tis. Kč

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

    0 tis. Kč