Informace o projektu
Correctness Analysis of C and C++ Programs with Threads
- 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
Journal of Systems and Software, rok: 2018, ročník: 143, vydání: Oct, DOI
2017
-
From Model Checking to Runtime Verification and Back
Runtime Verification - 17th International Conference, RV 2017, rok: 2017
-
Model Checking of C and C++ with DIVINE 4
Automated Technology for Verification and Analysis, rok: 2017
-
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
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
IEEE International Conference on Software Quality, Reliability and Security - QRS 2017, rok: 2017
2016
-
Control Explicit-Data Symbolic Model Checking
ACM Transactions on Software Engineering and Methodology, rok: 2016, ročník: 25, vydání: 2, DOI
-
DIVINE: Explicit-State LTL Model Checker
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
Science of Computer Programming, rok: 2016, ročník: 128, vydání: 15 October 2016, DOI
-
On verifying C++ programs with probabilities
Proceedings of the 31st Annual ACM Symposium on Applied Computing, rok: 2016
-
Optimal observation mode scheduling for systems under temporal constraints
2016 American Control Conference (ACC), rok: 2016