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
Odpovědnost: Vojnar Tomáš, prof. Ing., Ph.D.