Detail projektu

Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti

Období řešení: 1.1.2010 — 31.12.2013

Zdroje financování

Grantová agentura České republiky - Standardní projekty

O projektu

Automatizovaná verifikace programů je v současnosti s ohledem na rostoucí dopad počítačem řízených systémů na naše životy a výraznou potřebu minimalizovat počet chyb v těchto systémech velmi aktuálním výzkumným tématem. Projekt se konkrétně zaměřuje na verifikaci programů s pokročilými rysy paralelismu a neomezenosti, které patří k obzvláště problematickým aspektům software, se kterými se musí automatická verifikace vyrovnávat. V prvním případě se projekt soustřeďuje zejména na metody verifikace programů určených pro moderní vícejádrové procesory. V druhém případě se jedná o verifikaci programů pracujících s různými neomezenými datovými strukturami, zejména pak poli (o parametrické velikosti) a složitými dynamickými strukturami založenými na ukazatelích (jako jsou seznamy či stromy). Projekt zahrnuje výzkum metod dynamické i statické verifikace, včetně model checkingu, a také jejích vhodných kombinací. Pro práci s programy s nekonečnými stavovými prostory se výzkum v projektu zaměřuje na metody efektivní symbolické verifikace založené na použití automatů a logik.

Popis anglicky
Automated verification of programs is currently a very hot issue due to the rising influence of computer-controlled systems on our lives and the recognised need to minimise the number of errors in them. The project, in particular, considers verification of programs with advanced features of concurrency and unboundedness, which both belong among especially problematic features to be dealt with in automated verification. In the former case, the project pays a special attention to verification of applications intended to run on the current multi-core processors. In the latter case, verification of programs manipulating different unbounded structures, notably (parametrised-size) arrays and complex dynamic linked data structures (such as lists or trees), is considered. The project contains research on methods of dynamic as well as static verification, including model checking, and possibly their suitable combinations. For handling infinite-state programs, efficient symbolic verification methods based on automata and logics are the primary target of the research in the project.

Klíčová slova
automatická verifikace programů; statická a dynamická analýza; formální verifikace; model checking; paralelismus; nekonečně stavové programy; dynamické datové struktury

Klíčová slova anglicky
automated verification of programs; static and dynamic analysis; formal verification; model checking; concurrency; infinite-state programs; dynamic data structures

Označení

GAP103/10/0306

Originální jazyk

čeština

Řešitelé

Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitel
Dudka Kamil, Ing. - spoluřešitel
Dudka Vendula, Ing. - spoluřešitel
Fiedor Jan, Ing., Ph.D. - spoluřešitel
Gach Marek, Ing. - spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. - spoluřešitel
Hýsek Jiří, Ing. - spoluřešitel
Charvát Lukáš, Ing., Ph.D. - spoluřešitel
Konečný Filip, Ing., Ph.D. - spoluřešitel
Letko Zdeněk, Ing., Ph.D. - spoluřešitel
Šimáček Jiří, Ing., Ph.D. - spoluřešitel

Útvary

Fakulta informačních technologií
- odpovědné pracoviště (1.1.1989 - nezadáno)
Ústav inteligentních systémů
- odpovědné pracoviště (18.12.2009 - nezadáno)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (18.12.2009 - 31.12.2013)
Ústav inteligentních systémů
- spolupříjemce (18.12.2009 - 31.12.2013)
Fakulta informačních technologií
- příjemce (1.1.2010 - 31.12.2013)

Výsledky

HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013. p. 1-35.
Detail

HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013. p. 1-25.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013. p. 0-0.
Detail

ROGALEWICZ, A.; ŠIMÁČEK, J.; IOSIF, R. The Tree Width of Separation Logic with Recursive Definitions. arXiv:1301.5139: 2013. p. 0-0.
Detail

DUDKA, V.; KŘENA, B.; LETKO, Z.; VOJNAR, T. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno: 2012. p. 0-0.
Detail

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

ZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. FIT-TR-2011-05, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. FIT-TR-2011-02, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

ABDULLA, P.; CHEN, Y.; CLEMENTE, L.; HOLÍK, L.; HONG, C.; MAYR, R.; VOJNAR, T. Advanced Ramsey-based Büchi Automata Inclusion Testing. FIT-TR-2011-03, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
Detail

HOLÍK, L. Simulations and Antichains for Efficient Handling of Finite Automata. Brno: Department of Intelligent Systems FIT BUT, 2011. p. 0-0.
Detail

FIEDOR, J.; KŘENA, B.; LETKO, Z.; VOJNAR, T. A Uniform Classification of Common Concurrency Errors. FIT-TR-2010-03, Brno: 2010. p. 0-0.
Detail

KŘENA, B.; LETKO, Z.; VOJNAR, T.; UR, S. A Platform for Search-Based Testing of Concurrent Software. 6th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2010. p. 208-208. ISBN: 978-80-87342-10-7.
Detail

HOLÍK, L.; VOJNAR, T.; CHEN, Y.; MAYR, R.; HONG, C.; ABDULLA, P.; CLEMENTE, L. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010. p. 0-0.
Detail

FIEDOR, J.; DUDKA, V.; KŘENA, B.; LETKO, Z.; UR, S.; VOJNAR, T. Advances in Noise-based Testing of Concurrent Programs. Software Testing Verification and Reliability, 2015, vol. 25, no. 3, p. 272-309. ISSN: 1099-1689.
Detail

MÜLLER, P.; VOJNAR, T.: cpalien; CPAlien: Configurable Program Analysis over Symbolic Memory Graphs. http://www.fit.vutbr.cz/research/groups/verifit/tools/cpalien. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/cpalien. (software)
Detail

LETKO, Z. Analysis and Testing of Concurrent Programs. Information Sciences and Technologies Bulletin of the ACM Slovakia, 2013, vol. 5, no. 3, p. 1-8. ISSN: 1338-1237.
Detail

HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013. p. 224-239. ISBN: 978-3-319-02443-1.
Detail

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science, 2013, vol. 24, no. 2, p. 187-210. ISSN: 0129-0541.
Detail