Práce se slozitými datovými strukturami a paralelismem v prostredí Rich Model Toolkit
Hlavní resitel:Vojnar Tomás
Spoluresitelé:Ceska Milan, Krena Bohuslav, Peringer Petr, Rogalewicz Adam, Smrcka Ales
Dalsí resitelé:Dudka Kamil, Fiedor Jan, Gach Marek, Holík Lukás, Hrubá Vendula, Charvát Lukás, Konecný Filip, Letko Zdenek, Simácek Jirí
Agentura:MSMT
Kód:OC10009
Zacátek:2010
Konec:2012
Klícová slova:automatizovaná verifikace, programy se slozitými datovými strukturami, paralelní systémy, symbolická verifikace, statická a dynamická analýza, model checking, teorie automatu a logik
Anotace:
Projekt je príspevkem k výzkumu realizovanému v rámci COST akce IC0901: Rich Model Toolkit - An Infrastructure for Reliable Computer Systems, zamerené (1) na vývoj jazyka pro homogenní popis co nejsirsího spektra pocítacových systému pro potreby jejich následné verifikace a (2) na výzkum v oblasti metod formální verifikace s cílem výrazne zvýsit míru jejich obecnosti, efektivnosti a stupne automatizace. Výzkum v projektu se konkrétne zamerí na dva aspekty chování pocítacových systému predstavující významnou výzvu pro soucasné verifikacní prístupy, a to na práci se slozitými datovými strukturami (vcetne dynamických datových struktur zalozených na ukazatelích) a na pouzití paralelismu v moderních pocítacových systémech. V prvním prípade se bude jednat zejména o výzkum metod symbolické verifikace zalozených na aplikacích teorie automatu, logik a jejich kombinací. V druhém prípade 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 zpusobem významného zlepsení mozností verifikace soucasných masivne paralelních systému.

Produkty

2012HAVEN: Otevrený rámec pro akceleraci funkcní verifikace hardwaru pomocí FPGA, software, 2012
Autori: Simková Marcela, Lengál Ondrej, Kajan Michal
 Prostredí pro analýzu vícevláknových C/C++ programu na binární úrovni, software, 2012
Autori: Fiedor Jan, Vojnar Tomás
 VATA: Knihovna pro efektivní práci s nedeterministickými stromovými automaty, software, 2012
Autori: Lengál Ondrej, Simácek Jirí, Vojnar Tomás
2011Nástroj propojující dynamickou analýzu a bounded model checking, software, 2011
Autori: Fiedor Jan, Hrubá Vendula, Krena Bohuslav, Vojnar Tomás

Publikace

2013Abdulla, P., A., Cederberg, J., Vojnar, T.: Monotonic Abstraction for Programs with Multiply-Linked Structures, In: International Journal of Foundations of Computer Science, roc. 24, c. 2, 2013, SG, s. 187-210, ISSN 0129-0541
 Krena, B., Vojnar, T.: Automated formal analysis and verification: an overview, In: International Journal of General Systems, roc. 2013, c. 42, Abingdon, GB, s. 335-365, ISSN 0308-1079
2012Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular (Tree) Model Checking, In: International Journal on Software Tools for Technology Transfer, roc. 14, c. 2, 2012, DE, s. 167-191, ISSN 1433-2779
 Ceska, M., Fiedor, J., Gach, M.: A Novel Approach to Modechart Verification of Real-Time systems, In: Lecture Notes in Computer Science, roc. 2012, c. 6927, DE, s. 559-567, ISSN 0302-9743
 Dudka, K., Müller, P., Peringer, P., Vojnar, T.: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution), In: Lecture Notes in Computer Science, roc. 2012, c. 7214, DE, s. 544-547, ISSN 0302-9743
 Dudka, K., Peringer, P., Vojnar, T.: An Easy to Use Infrastructure for Building Static Analysis Tools, In: Lecture Notes in Computer Science, roc. 2012, c. 6927, DE, s. 527-534, ISSN 0302-9743
 Fiedor, J., Hrubá, V., Krena, B., Vojnar, T.: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, In: Lecture Notes in Computer Science, roc. 2012, c. 7186, DE, s. 5, ISSN 0302-9743
 Fiedor, J., Krena, B., Letko, Z., Vojnar, T.: A Uniform Classification of Common Concurrency Errors, In: Lecture Notes in Computer Science, roc. 2012, c. 6927, DE, s. 519-526, ISSN 0302-9743
 Fiedor, J., Vojnar, T.: ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, In: Lecture Notes in Computer Science, roc. 2012, c. 7687, DE, s. 35-41, ISSN 0302-9743
 Fiedor, J., Vojnar, T.: 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, P., Holík, L., Rogalewicz, A., Simácek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation, In: Formal Methods in System Design, roc. 2012, c. 41, Berlin, DE, s. 83-106, ISSN 0925-9856
 Hrubá, V., Krena, B., Letko, Z., Ur, S., Vojnar, T.: Testování vícevláknových aplikací pomocí genetických algoritmu, In: Lecture Notes in Computer Science, roc. 2012, c. 7515, DE, s. 152-167, ISSN 0302-9743
 Hrubá, V., Krena, B., Letko, Z., Vojnar, T.: Testing of Concurrent Programs Using Genetic Algorithms, FIT-TR-2012-01, Brno, CZ, 2012, s. 31
 Charvát, L., Smrcka, A., Vojnar, T.: 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, R., Hojjat, H., Konecný, F., Kuncak, V., Rummer, P.: Accelerating Interpolants, In: Lecture Notes in Computer Science, roc. 2012, c. 7561, DE, s. 187-202, ISSN 0302-9743
 Konecný, F., Hojjat, H., Iosif, R., Kuncak, V., Rummer, P., Garnier, F.: A Verification Toolkit for Numerical Transition Systems, In: Lecture Notes in Computer Science, roc. 2012, c. 7436, DE, s. 247-251, ISSN 0302-9743
 Konecný, F., Iosif, R., Bozga, M.: Deciding Conditional Termination, In: Lecture Notes in Computer Science, roc. 2012, c. 7214, DE, s. 252-266, ISSN 0302-9743
 Krena, B., Letko, Z., Vojnar, T.: Analysis and Testing of Concurrent Programs, Brno, CZ, FIT VUT, 2012, s. 136, ISBN 978-80-214-4464-5
 Krena, B., Letko, Z., Vojnar, T.: Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software, In: Lecture Notes in Computer Science, roc. 2012, c. 7186, DE, s. 177-192, ISSN 0302-9743
 Krena, B., Letko, Z., Vojnar, T.: Noise Injection Heuristics for Concurrency Testing, In: Lecture Notes in Computer Science, roc. 2012, c. 7119, DE, s. 123-131, ISSN 0302-9743
 Lengál, O., Simácek, J., Vojnar, T.: VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, In: Lecture Notes in Computer Science, roc. 2012, c. 7214, DE, s. 79-94, ISSN 0302-9743
 Simková, M., Lengál, O., Kajan, M.: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, In: Lecture Notes in Computer Science, roc. 2012, c. 7261, DE, s. 247-253, ISSN 0302-9743
2011Abdulla, P., A., Cederberg, J., Vojnar, T.: Monotonic Abstraction for Programs with Multiply-Linked Structures, In: Lecture Notes in Computer Science, roc. 2011, c. 6945, DE, s. 125-138, ISSN 0302-9743
 Abdulla, P., A., 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, CZ, FIT VUT, 2011, s. 45
 Abdulla, P., A., Chen, Y., Clemente, L., Holík, L., Hong, C., Mayr, R., Vojnar, T.: Advanced Ramsey-based Büchi Automata Inclusion Testing, In: Lecture Notes in Computer Science, roc. 2011, c. 6901, DE, s. 187-202, ISSN 0302-9743
 Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists are Counter Automata, In: Formal Methods in System Design, roc. 38, c. 2, 2011, Berlin, DE, s. 158-192, ISSN 0925-9856
 Ceska, M., Fiedor, J., Gach, M.: 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, K., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, In: Lecture Notes in Computer Science, roc. 2011, c. 6806, DE, s. 372-378, ISSN 0302-9743
 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, CZ, FIT VUT, 2011, s. 23
 Fiedor, J., Hrubá, V., Krena, B., Vojnar, T.: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, FIT-TR-2011-06, Brno, CZ, FIT VUT, 2011, s. 9
 Fiedor, J., Krena, B., Letko, Z., Vojnar, T.: 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, P., Holík, L., Rogalewicz, A., Simácek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation, In: Lecture Notes in Computer Science, roc. 2011, c. 6806, DE, s. 424-440, ISSN 0302-9743
 Habermehl, P., Holík, L., Rogalewicz, A., Simácek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation, FIT-TR-2011-01, Brno, CZ, FIT VUT, 2011, s. 30
 Holík, L., Lengál, O., Simácek, J., Vojnar, T.: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, In: Lecture Notes in Computer Science, roc. 2011, c. 6996, DE, s. 243-258, ISSN 0302-9743
 Holík, L., Lengál, O., Simácek, J., Vojnar, T.: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, FIT-TR-2011-04, Brno, CZ, FIT VUT, 2011, s. 22
 Holík, L.: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, s. 128
 Simková, M., Lengál, O., Kajan, M.: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, FIT-TR-2011-05, Brno, CZ, FIT VUT, 2011, s. 16
2010Abdulla, P., A., Clemente, L., Holík, L., Hong, C., Chen, Y., Mayr, R., Vojnar, T.: Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, FIT-TR-2010-02, Brno, CZ, FIT VUT, 2010, s. 30
 Abdulla, P., A., Clemente, L., Holík, L., Hong, C., Chen, Y., Mayr, R., Vojnar, T.: 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, P., A., Holík, L., Chen, Y., Mayr, R., Vojnar, T.: 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, P., A., Holík, L., Chen, Y., Mayr, R., Vojnar, T.: 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, M., Iosif, R., Konecný, F.: Fast Acceleration of Ultimately Periodic Relations, In: Computer Aided Verification, Berlin, DE, Springer, 2010, s. 227-242, ISBN 978-3-642-14294-9
 Fiedor, J., Krena, B., Letko, Z., Vojnar, T.: A Uniform Classification of Common Concurrency Errors, FIT-TR-2010-03, Brno, CZ, 2010, s. 24
 Holík, L., Vojnar, T.: Simulations and Aintichains for Efficient Handling of Tree Automata, Brno, CZ, FIT VUT, 2010, s. 150, ISBN 978-80-214-4217-7
 Krena, B., Letko, Z., Ur, S., Vojnar, T.: A Platform for Search-Based Testing of Concurrent Software, In: PADTAD '10, Trento, IT, ACM, 2010, s. 11, ISBN 978-1-60558-823-0

Vase IPv4 adresa: 107.20.7.65
Prepnout na IPv6 spojení

DNSSEC [dnssec]