Informace o projektu
Abstrakce a jiné techniky v semi-symbolické verifikaci programů
- Kód projektu
- GA18-02177S
- Období řešení
- 1/2018 - 12/2020
- 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í analýzu a verifikaci počítačových programů zapsaných v programovacích jazycích C a C++. Konkrétně se projekt zaměřuje na využití abstrakcí, které jsou realizované jako spekulativní předpoklady kladené na běh verifikovaného programu. Programy, které jsou anotovány spekulativními předpoklady, je méně náročné verifikovat, avšak v případě předpokladů, které nejsou pravdivé, může být výsledek verifikace nekorektní. Cílem projektu je vystavět teorii spekulativních předpokladů, jejichž neplatnost bude možné detekovat samotnou procedurou verifikace, a tuto teorii realizovat ve vhodném verifikačním prostředí. Toto prostředí bude nad rámec uvedené metody zahrnovat využití dalších relevantních technik verifikace a analýzy programů (prořezávání kódu, řešení SMT dotazů, a pod.), které v souhrnu povedou k větší efektivitě procedury verifikace.
Publikace
Počet publikací: 22
2021
-
Reproducible execution of POSIX programs with DiOS
Software & Systems Modeling, rok: 2021, ročník: 20, vydání: 2, DOI
-
Symbiotic 6: generating test cases by slicing and symbolic execution
International Journal on Software Tools for Technology Transfer, rok: 2021, ročník: 23, vydání: 6, DOI
2020
-
Abstracting Strings for Model Checking of C Programs
Applied Sciences, rok: 2020, ročník: 10, vydání: 21, DOI
-
DG: A program analysis library
Software Impacts, rok: 2020, ročník: 2020, vydání: 6, DOI
-
DG: Analysis and Slicing of LLVM Bitcode
The 18?? International Symposium on Automated Technology for Verification and Analysis, rok: 2020
-
Joint Forces for Memory Safety Checking Revisited
-
On Symbolic Execution of Decompiled Programs
Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020, rok: 2020
-
Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, rok: 2020
-
Symbiotic 7: Integration of Predator and More (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems, rok: 2020
2019
-
A Simulator for LLVM Bitcode
24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019, rok: 2019