Detail projektu

Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit

Období řešení: 01.01.2010 — 31.12.2012

Zdroje financování

Ministerstvo školství, mládeže a tělovýchovy ČR - COST

- částečně financující (2010-05-01 - 2012-12-31)

O projektu

Projekt je příspěvkem k výzkumu realizovanému v rámci COST akce IC0901: Rich Model Toolkit - An Infrastructure for Reliable Computer Systems, zaměřené (1) na vývoj jazyka pro homogenní popis co nejširšího spektra počítačových systémů pro potřeby jejich následné verifikace a (2) na výzkum v oblasti metod formální verifikace s cílem výrazně zvýšit míru jejich obecnosti, efektivnosti a stupně automatizace. Výzkum v projektu se konkrétně zaměří na dva aspekty chování počítačových systémů představující významnou výzvu pro současné verifikační přístupy, a to na práci se složitými datovými strukturami (včetně dynamických datových struktur založených na ukazatelích) a na použití paralelismu v moderních počítačových systémech. V prvním případě se bude jednat zejména o výzkum metod symbolické verifikace založených na aplikacích teorie automatů, logik a jejich kombinací. V druhém případě pak o výzkum v oblasti model checkingu, statické analýzy, dynamické analýzy i jejich vhodných kombinací s cílem dosáhnout tímto způsobem významného zlepšení možností verifikace současných masivně paralelních systémů.

Popis anglicky
The project contributes to the research planned within the COST action IC0901: Rich Model Toolkit - An Infrastructure for Reliable Computer Systems, which is targeted at (1) development of a language for describing in a homogeneous way a broad range of computer systems to be verified and (2) research in the area of methods for formal verification with the goal of significantly increasing their generality, efficiency, and degree of automation. The proposed project in particular considers two aspects of the systems dealt with in the COST action IC0901 that constitute a very significant challenge for the current verification methods. Namely, the project considers development of new verification methods for computer systems with complex data structures (including dynamic data structures based on pointers) and/or with advanced features of concurrency. In the former case, the project concentrates on research on symbolic verification methods based on the theory of automata, logics, and their combinations. In the latter case, the project pursues research in the areas of model checking, static analysis, dynamic analysis as well as their suitable combinations aimed at significantly improving their capabilities for verification of modern massively concurrent systems.

Klíčová slova
automatizovaná verifikace, programy se složitými datovými strukturami, paralelní systémy, symbolická verifikace, statická a dynamická analýza, model checking, teorie automatů a logik

Klíčová slova anglicky
Automated verification, programs with complex data structures, concurrent systems, symbolic verification, static and dynamic analysis, model checking, theory of automata and logics

Označení

OC10009

Originální jazyk

čeština

Řešitelé

Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitel

Útvary

Fakulta informačních technologií
- příjemce (01.05.2010 - 31.12.2012)

Výsledky

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlín: Springer Verlag, 2010. p. 158-174. ISBN: 978-3-642-12001-5.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. 2013. p. 42-42.
Detail

KŘENA, B.; LETKO, Z.; UR, S.; VOJNAR, T. A Platform for Search-Based Testing of Concurrent Software. PADTAD '10. Proceedings of the 8th Workshop on Parallel and Distributed Systems. Trento: Association for Computing Machinery, 2010. p. 48-58. ISBN: 978-1-60558-823-0.
Detail

BOZGA, M.; IOSIF, R.; KONEČNÝ, F. Fast Acceleration of Ultimately Periodic Relations. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2010. p. 227-242. ISBN: 978-3-642-14294-9.
Detail

HOLÍK, L.; VOJNAR, T. Simulations and Aintichains for Efficient Handling of Tree Automata. FIT Monograph. FIT Monograph. Brno: Faculty of Information Technology BUT, 2010. 150 p. ISBN: 978-80-214-4217-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. Computer Aided Verification. Lecture Notes in Computer Science. Berlín: Springer Verlag, 2010. p. 132-147. ISBN: 978-3-642-14294-9.
Detail

DUDKA, V.; KŘENA, B.; LETKO, Z.; UR, S.; VOJNAR, T. Testing of Concurrent Programs with Genetic Algorithms. 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2012. p. 0-0. ISBN: 978-80-87342-15-2.
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

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). FIT-TR-2010-01, Brno: Faculty of Information Technology BUT, 2010. p. 0-0.
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

ZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: 2012. p. 1 (1 s.).
Detail

HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6806, p. 424-440. ISSN: 0302-9743.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6806, p. 372-378. ISSN: 0302-9743.
Detail

VOJNAR, T.; IOSIF, R.; HABERMEHL, P.; BOUAJJANI, A.; BOZGA, M.; MORO, P. Programs with Lists are Counter Automata. FORMAL METHODS IN SYSTEM DESIGN, 2011, vol. 38, no. 2, p. 158-192. ISSN: 0925-9856.
Detail

HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6996, p. 243-258. ISSN: 0302-9743.
Detail

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P. Monotonic Abstraction for Programs with Multiply-Linked Structures. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6945, p. 125-138. ISSN: 0302-9743.
Detail

ABDULLA, P.; CHEN, Y.; CLEMENTE, L.; HOLÍK, L.; HONG, C.; MAYR, R.; VOJNAR, T. Advanced Ramsey-based Büchi Automata Inclusion Testing. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6901, p. 187-202. ISSN: 0302-9743.
Detail

ZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7261, p. 247-253. ISSN: 0302-9743.
Detail

FIEDOR, J.; GACH, M.; ČEŠKA, M. A Novel Approach to Modechart Verification of Real-Time systems. Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: The Universidad de Las Palmas de Gran Canaria, 2011. p. 338-339. ISBN: 978-84-693-9560-8.
Detail

FIEDOR, J.; LETKO, Z.; VOJNAR, T.; KŘENA, B. A Uniform Classification of Common Concurrency Errors. Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: The Universidad de Las Palmas de Gran Canaria, 2011. p. 326-327. ISBN: 978-84-693-9560-8.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. An Easy to Use Infrastructure for Building Static Analysis Tools. Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: The Universidad de Las Palmas de Gran Canaria, 2011. p. 328-329. ISBN: 978-84-693-9560-8.
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B. Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software. Lecture Notes in Computer Science, 2012, roč. 2012, č. 7186, s. 177-192. ISSN: 0302-9743.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. An Easy to Use Infrastructure for Building Static Analysis Tools. Lecture Notes in Computer Science, 2012, vol. 2012, no. 6927, p. 527-534. ISSN: 0302-9743.
Detail

FIEDOR, J.; KŘENA, B.; LETKO, Z.; VOJNAR, T. A Uniform Classification of Common Concurrency Errors. Lecture Notes in Computer Science, 2012, vol. 2012, no. 6927, p. 519-526. ISSN: 0302-9743.
Detail

ČEŠKA, M.; FIEDOR, J.; GACH, M. A Novel Approach to Modechart Verification of Real-Time systems. Lecture Notes in Computer Science, 2012, vol. 2012, no. 6927, p. 559-567. ISSN: 0302-9743.
Detail

KONEČNÝ, F.; IOSIF, R.; BOZGA, M. Deciding Conditional Termination. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 252-266. ISSN: 0302-9743.
Detail

KŘENA, B.; LETKO, Z.; VOJNAR, T. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7119, p. 123-131. ISSN: 0302-9743.
Detail

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7186, p. 1-5. ISSN: 0302-9743.
Detail

LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 79-94. ISSN: 0302-9743.
Detail

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 544-547. ISSN: 0302-9743.
Detail

ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, 2012, vol. 14, no. 2, p. 167-191. ISSN: 1433-2779.
Detail

HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FORMAL METHODS IN SYSTEM DESIGN, 2012, vol. 2012, no. 41, p. 83-106. ISSN: 0925-9856.
Detail

DUDKA, V.; KŘENA, B.; LETKO, Z.; UR, S.; VOJNAR, T. Testování vícevláknových aplikací pomocí genetických algoritmů. Lecture Notes in Computer Science, 2012, roč. 2012, č. 7515, s. 152-167. ISSN: 0302-9743.
Detail

KONEČNÝ, F.; HOJJAT, H.; IOSIF, R.; KUNCAK, V.; RUMMER, P.; GARNIER, F. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7436, p. 247-251. ISSN: 0302-9743.
Detail

FIEDOR, J.; VOJNAR, T. Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. PADTAD '12. Proceedings of the 10th Workshop on Parallel and Distributed Systems. New York: Association for Computing Machinery, 2012. p. 36-46. ISBN: 978-1-4503-1456-5.
Detail

IOSIF, R.; HOJJAT, H.; KONEČNÝ, F.; KUNCAK, V.; RUMMER, P. Accelerating Interpolants. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7561, p. 187-202. ISSN: 0302-9743.
Detail

FIEDOR, J.; VOJNAR, T. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7687, p. 35-41. ISSN: 0302-9743.
Detail

KŘENA, B.; LETKO, Z.; VOJNAR, T. Analysis and Testing of Concurrent Programs. FIT Monograph. FIT Monograph. Brno: Faculty of Information Technology BUT, 2012. 136 p. ISBN: 978-80-214-4464-5.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012. p. 6-12. ISBN: 978-1-4673-4441-8.
Detail

VOJNAR, T.; KŘENA, B. Automated formal analysis and verification: an overview. INTERNATIONAL JOURNAL OF GENERAL SYSTEMS, 2013, vol. 2013, no. 42, p. 335-365. ISSN: 0308-1079.
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

FIEDOR, J.; VOJNAR, T.: ANaConDA; ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. http://www.fit.vutbr.cz/research/groups/verifit/tools/anaconda/. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/anaconda/. (software)
Detail

ZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M.: haven; HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Nástroj i dokumentaci lze získat na URL http://www.fit.vutbr.cz/~isimkova/haven/ (http://www.fit.vutbr.cz/%7Eisimkova/haven/). URL: https://www.fit.vut.cz/research/product/234/. (software)
Detail

LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.: vata; VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata/. URL: https://www.fit.vut.cz/research/product/223/. (software)
Detail

DUDKA, V.; FIEDOR, J.; VOJNAR, T.; KŘENA, B.: DA-BMC; A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. http://www.fit.vutbr.cz/research/groups/verifit/tools/da-bmc. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/da-bmc. (software)
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T.: predator; Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic.    - http://www.fit.vutbr.cz/research/groups/verifit/tools/predator. URL: https://www.fit.vut.cz/research/product/149/. (software)
Detail

ŠIMÁČEK, J.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.: fapointers; Forester: A Tool for Verification of Programs with Pointers. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/forester/. URL: https://www.fit.vut.cz/research/product/142/. (software)
Detail

DUDKA, V.; FIEDOR, J.; KŘENA, B.; LETKO, Z.; VOJNAR, T.: RecRev; Replay Tracer & BMC. http://www.fit.vutbr.cz/research/groups/verifit/tools/RecRev. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/RecRev. (software)
Detail

FIEDOR, J.; GACH, M.; ČEŠKA, M.: zetav; Tool for verification of systems specified in RT-Logic language. http://www.fit.vutbr.cz/research/groups/verifit/tools/zetav. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/zetav. (software)
Detail

LENGÁL, O.; HOLÍK, L.; VOJNAR, T.: libSFTA; libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype. https://github.com/ondrik/libsfta. URL: https://github.com/ondrik/libsfta. (software)
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T.: code-listener; An Easy to Use Infrastructure for Building Static Analysis Tools.    - http://www.fit.vutbr.cz/research/groups/verifit/tools/code-listener. URL: https://www.fit.vut.cz/research/product/150/. (software)
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B.: SearchBestie; Search-based Testing Environment (SearchBestie). http://www.fit.vutbr.cz/research/groups/verifit/tools/SearchBestie. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/SearchBestie. (software)
Detail

ŠIMÁČEK, J.; HOLÍK, L.; VOJNAR, T.: SA; Tool for Computing Simulations. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/sa/. URL: https://www.fit.vut.cz/research/product/131/. (software)
Detail

KONEČNÝ, F.; VOJNAR, T.; BOZGA, M.; IOSIF, R.: FLATA; FLATA. http://www-verimag.imag.fr/FLATA.html. URL: http://www-verimag.imag.fr/FLATA.html. (software)
Detail

GACH, M.; FIEDOR, J.; ČEŠKA, M.: verif; Tool for verification of systems described using the Modechart formalism. http://www.fit.vutbr.cz/research/groups/verifit/tools/verif. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/verif. (software)
Detail

Odpovědnost: Vojnar Tomáš, prof. Ing., Ph.D.