Detail projektu

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

Období řešení: 1. 1. 2010 – 31. 12. 2012

Typ projektu: grant

Kód: OC10009

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

Program: COST

Název anglicky
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
Typ
grant
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

Abstrakt

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ů.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS) – hlavní řešitel
Publikace

2013

  • 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
  • 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

2012

  • Č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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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. 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
  • 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
  • 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
  • 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
  • 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
  • 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

2011

  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

2010

  • 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.; 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
  • 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
  • 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
Nahoru