Informace o projektu
Correctness Analysis of C and C++ Programs with Threads

Informace

Projekt nespadá pod Lékařskou fakultu, ale pod Fakultu informatiky. Oficiální stránka projektu je na webu muni.cz.

Kód projektu

GA15-08772S

Období řešení

3/2015 - 12/2017

Investor / Programový rámec / typ projektu

Grantová agentura ČR

Standardní projekty

Fakulta / Pracoviště MU

Fakulta informatiky

Projekt se zaměřuje na výzkum a vývoj nových algoritmů a datových struktur, které umožní efektivní verifikaci vícevláknových programů zapsaných v programovacích jazycích C a C++ metodou ověřování modelu (angl. model checking). Konkrétním cílem projektu je vyvinout nové metody automatické abstrakce programů vstupujících do procesu verifikace, které budou realizované formou transformace těchto programů. Dále pak získat nové metody umožňující kombinaci explicitního a symbolického přístupu k verifikaci metodou ověřování modelu, či metody umožňující jiným způsobem redukovat prostorové nároky verifikačních nástrojů. Pro učely porovnání a vyhodnocení budou nově vyvinuté algoritmy a datové struktury integrovány do experimentálního softwarového nástroje DIVINE. To mimojiné umožní efektivní využití stávajících výpočetních architektur (více-jádrové počítače, výpočetní klastry) tak, aby byla významně posunuta hranice systémů, jež je možné doposud verifikovat automatizovanými metodami formální verifikace.

Publikace

Počet publikací: 15

2018

DiVM: Model checking with LLVM and graph memory

ROČKAI Petr ŠTILL Vladimír ČERNÁ Ivana BARNAT Jiří

Článek v odborném periodiku

Journal of Systems and Software, rok: 2018, ročník: 143, vydání: Oct, DOI

2017

From Model Checking to Runtime Verification and Back

KEJSTOVÁ Katarína ROČKAI Petr BARNAT Jiří

Článek ve sborníku

Runtime Verification - 17th International Conference, RV 2017, rok: 2017
Model Checking of C and C++ with DIVINE 4

BARANOVÁ Zuzana BARNAT Jiří KEJSTOVÁ Katarína KUČERA Tadeáš LAUKO Henrich MRÁZEK Jan ROČKAI Petr ŠTILL Vladimír

Článek ve sborníku

Automated Technology for Verification and Analysis, rok: 2017
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)

MRÁZEK Jan JONÁŠ Martin ŠTILL Vladimír LAUKO Henrich BARNAT Jiří

Článek ve sborníku

Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II, rok: 2017
Using Off-the-Shelf Exception Support Components in C++ Verification

ŠTILL Vladimír ROČKAI Petr BARNAT Jiří

Článek ve sborníku

IEEE International Conference on Software Quality, Reliability and Security - QRS 2017, rok: 2017

2016

Control Explicit-Data Symbolic Model Checking

BAUCH Petr HAVEL Vojtěch BARNAT Jiří

Článek v odborném periodiku

ACM Transactions on Software Engineering and Methodology, rok: 2016, ročník: 25, vydání: 2, DOI
DIVINE: Explicit-State LTL Model Checker

ŠTILL Vladimír ROČKAI Petr BARNAT Jiří

Článek ve sborníku

Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, rok: 2016
Model checking C++ programs with exceptions

ROČKAI Petr BARNAT Jiří BRIM Luboš

Článek v odborném periodiku

Science of Computer Programming, rok: 2016, ročník: 128, vydání: 15 October 2016, DOI
On verifying C++ programs with probabilities

BARNAT Jiří ČERNÁ Ivana ROČKAI Petr ŠTILL Vladimír ZÁKOPČANOVÁ Kristína

Článek ve sborníku

Proceedings of the 31st Annual ACM Symposium on Applied Computing, rok: 2016
Optimal observation mode scheduling for systems under temporal constraints

TESAŘOVÁ Eva SVOREŇOVÁ Mária BARNAT Jiří ČERNÁ Ivana

Článek ve sborníku

2016 American Control Conference (ACC), rok: 2016