Ústav inteligentních systémů

Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit
Hlavní řešitel:Vojnar Tomáš
Spoluřešitelé:Češka Milan, Křena Bohuslav, Peringer Petr, Rogalewicz Adam, Smrčka Aleš
Další řešitelé:Dudka Kamil, Fiedor Jan, Gach Marek, Holík Lukáš, Hrubá Vendula, Charvát Lukáš, Konečný Filip, Letko Zdeněk, Šimáček Jiří
Agentura:MŠMT
Kód:OC10009
Začátek:2010
Konec:2012
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
Anotace:
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ů.

Produkty

2012HAVEN: Otevřený rámec pro akceleraci funkční verifikace hardwaru pomocí FPGA, software, 2012
Autoři: Šimková Marcela, Lengál Ondřej, Kajan Michal
 Prostředí pro analýzu vícevláknových C/C++ programů na binární úrovni, software, 2012
Autoři: Fiedor Jan, Vojnar Tomáš
 VATA: Knihovna pro efektivní práci s nedeterministickými stromovými automaty, software, 2012
Autoři: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš
2011Nástroj propojující dynamickou analýzu a bounded model checking, software, 2011
Autoři: Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš

Publikace

2013Abdulla Parosh A., Cederberg Jonathan, Vojnar Tomáš: Monotonic Abstraction for Programs with Multiply-Linked Structures, In: International Journal of Foundations of Computer Science, roč. 24, č. 2, 2013, SG, s. 187-210, ISSN 0129-0541
 Křena Bohuslav, Vojnar Tomáš: Automated formal analysis and verification: an overview, In: International Journal of General Systems, roč. 2013, č. 42, Abingdon, GB, s. 335-365, ISSN 0308-1079
2012Bouajjani Ahmed, Habermehl Peter, Rogalewicz Adam, Vojnar Tomáš: Abstract Regular (Tree) Model Checking, In: International Journal on Software Tools for Technology Transfer, roč. 14, č. 2, 2012, DE, s. 167-191, ISSN 1433-2779
 Češka Milan, Fiedor Jan, Gach Marek: A Novel Approach to Modechart Verification of Real-Time systems, In: Lecture Notes in Computer Science, roč. 2012, č. 6927, DE, s. 559-567, ISSN 0302-9743
 Dudka Kamil, Müller Petr, Peringer Petr, Vojnar Tomáš: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution), In: Lecture Notes in Computer Science, roč. 2012, č. 7214, DE, s. 544-547, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: An Easy to Use Infrastructure for Building Static Analysis Tools, In: Lecture Notes in Computer Science, roč. 2012, č. 6927, DE, s. 527-534, ISSN 0302-9743
 Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, In: Lecture Notes in Computer Science, roč. 2012, č. 7186, DE, s. 5, ISSN 0302-9743
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: A Uniform Classification of Common Concurrency Errors, In: Lecture Notes in Computer Science, roč. 2012, č. 6927, DE, s. 519-526, ISSN 0302-9743
 Fiedor Jan, Vojnar Tomáš: ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, In: Lecture Notes in Computer Science, roč. 2012, č. 7687, DE, s. 35-41, ISSN 0302-9743
 Fiedor Jan, Vojnar Tomáš: Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level, In: PADTAD '12, New York, US, ACM, 2012, s. 36-46, ISBN 978-1-4503-1456-5
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, In: Formal Methods in System Design, roč. 2012, č. 41, Berlin, DE, s. 83-106, ISSN 0925-9856
 Hrubá Vendula, Křena Bohuslav, Letko Zdeněk, Ur Shmuel, Vojnar Tomáš: Testování vícevláknových aplikací pomocí genetických algoritmů, In: Lecture Notes in Computer Science, roč. 2012, č. 7515, DE, s. 152-167, ISSN 0302-9743
 Hrubá Vendula, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Testing of Concurrent Programs Using Genetic Algorithms, FIT-TR-2012-01, Brno, CZ, 2012, s. 31
 Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš: Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description, In: Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012), Austin, TX, US, IEEE, 2012, s. 6-12, ISBN 978-1-4673-4441-8
 Iosif Radu, Hojjat Hossein, Konečný Filip, Kuncak Viktor, Rummer Philipp: Accelerating Interpolants, In: Lecture Notes in Computer Science, roč. 2012, č. 7561, DE, s. 187-202, ISSN 0302-9743
 Konečný Filip, Hojjat Hossein, Iosif Radu, Kuncak Viktor, Rummer Philipp, Garnier Florent: A Verification Toolkit for Numerical Transition Systems, In: Lecture Notes in Computer Science, roč. 2012, č. 7436, DE, s. 247-251, ISSN 0302-9743
 Konečný Filip, Iosif Radu, Bozga Marius: Deciding Conditional Termination, In: Lecture Notes in Computer Science, roč. 2012, č. 7214, DE, s. 252-266, ISSN 0302-9743
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Analysis and Testing of Concurrent Programs, Brno, CZ, FIT VUT, 2012, s. 136, ISBN 978-80-214-4464-5
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software, In: Lecture Notes in Computer Science, roč. 2012, č. 7186, DE, s. 177-192, ISSN 0302-9743
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Noise Injection Heuristics for Concurrency Testing, In: Lecture Notes in Computer Science, roč. 2012, č. 7119, DE, s. 123-131, ISSN 0302-9743
 Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, In: Lecture Notes in Computer Science, roč. 2012, č. 7214, DE, s. 79-94, ISSN 0302-9743
 Šimková Marcela, Lengál Ondřej, Kajan Michal: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, In: Lecture Notes in Computer Science, roč. 2012, č. 7261, DE, s. 247-253, ISSN 0302-9743
2011Abdulla Parosh A., Cederberg Jonathan, Vojnar Tomáš: Monotonic Abstraction for Programs with Multiply-Linked Structures, In: Lecture Notes in Computer Science, roč. 2011, č. 6945, DE, s. 125-138, ISSN 0302-9743
 Abdulla Parosh A., Chen Yu-Fang, Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Mayr Richard, Vojnar Tomáš: Advanced Ramsey-based Büchi Automata Inclusion Testing, FIT-TR-2011-03, Brno, CZ, FIT VUT, 2011, s. 45
 Abdulla Parosh A., Chen Yu-Fang, Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Mayr Richard, Vojnar Tomáš: Advanced Ramsey-based Büchi Automata Inclusion Testing, In: Lecture Notes in Computer Science, roč. 2011, č. 6901, DE, s. 187-202, ISSN 0302-9743
 Bouajjani Ahmed, Bozga Marius, Habermehl Peter, Iosif Radu, Moro Pierre, Vojnar Tomáš: Programs with Lists are Counter Automata, In: Formal Methods in System Design, roč. 38, č. 2, 2011, Berlin, DE, s. 158-192, ISSN 0925-9856
 Češka Milan, Fiedor Jan, Gach Marek: A Novel Approach to Modechart Verification of Real-Time Systems, In: Proceedings of the 13th International Conference on Computer Aided Systems Theory, Universidad de Las Palmas de Canaria, ES, IUCTC, 2011, s. 338-339, ISBN 978-84-693-9560-8
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: An Easy to Use Infrastructure for Building Static Analysis Tools, In: Proceedings of the 13th International Conference on Computer Aided Systems Theory, Universidad de Las Palmas de Canaria, ES, IUCTC, 2011, s. 328-329, ISBN 978-84-693-9560-8
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, In: Lecture Notes in Computer Science, roč. 2011, č. 6806, DE, s. 372-378, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, FIT-TR-2011-02, Brno, CZ, FIT VUT, 2011, s. 23
 Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, FIT-TR-2011-06, Brno, CZ, FIT VUT, 2011, s. 9
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: A Uniform Classification of Common Concurrency Errors, In: Proceedings of the 13th International Conference on Computer Aided Systems Theory, Universidad de Las Palmas de Canaria, ES, IUCTC, 2011, s. 326-327, ISBN 978-84-693-9560-8
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, In: Lecture Notes in Computer Science, roč. 2011, č. 6806, DE, s. 424-440, ISSN 0302-9743
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, FIT-TR-2011-01, Brno, CZ, FIT VUT, 2011, s. 30
 Holík Lukáš, Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, In: Lecture Notes in Computer Science, roč. 2011, č. 6996, DE, s. 243-258, ISSN 0302-9743
 Holík Lukáš, Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, FIT-TR-2011-04, Brno, CZ, FIT VUT, 2011, s. 22
 Holík Lukáš: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, s. 128
 Šimková Marcela, Lengál Ondřej, Kajan Michal: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, FIT-TR-2011-05, Brno, CZ, FIT VUT, 2011, s. 16
2010Abdulla Parosh A., Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, FIT-TR-2010-02, Brno, CZ, FIT VUT, 2010, s. 30
 Abdulla Parosh A., Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing, In: Computer Aided Verification, Berlín, DE, Springer, 2010, s. 132-147, ISBN 978-3-642-14294-9
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata), FIT-TR-2010-01, Brno, CZ, FIT VUT, 2010, s. 22
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata), In: Tools and Algorithms for the Construction and Analysis of Systems, Berlín, DE, Springer, 2010, s. 158-174, ISBN 978-3-642-12001-5
 Bozga Marius, Iosif Radu, Konečný Filip: Fast Acceleration of Ultimately Periodic Relations, In: Computer Aided Verification, Berlin, DE, Springer, 2010, s. 227-242, ISBN 978-3-642-14294-9
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: A Uniform Classification of Common Concurrency Errors, FIT-TR-2010-03, Brno, CZ, 2010, s. 24
 Holík Lukáš, Vojnar Tomáš: Simulations and Aintichains for Efficient Handling of Tree Automata, Brno, CZ, FIT VUT, 2010, s. 150, ISBN 978-80-214-4217-7
 Křena Bohuslav, Letko Zdeněk, Ur Shmuel, Vojnar Tomáš: A Platform for Search-Based Testing of Concurrent Software, In: PADTAD '10, Trento, IT, ACM, 2010, s. 11, ISBN 978-1-60558-823-0

Vaše IPv4 adresa: 107.21.156.140
Přepnout na IPv6 spojení

DNSSEC [dnssec]