Project Details
Rich-Model Toolkit -- An Infrastructure for Reliable Computer Systems
Project Period: 30. 10. 2009 - 30. 10. 2013
Project Type: grant
Code: IC0901
Agency: COST, European Cooperation in Science and Technology
Program:
formal modelling, formal verification, decision procedures, synthesis
The main objective is making automated reasoning techniques and tools applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers. The Action coordinates activities on developing infrastructures for automated reasoning about the new notion of Rich Models of computer systems. Rich Models have the expressive power of a large fragment of formalizable mathematics, enabling specification of software, hardware, embedded, and distributed systems. Rich Models support modeling at a wide range of abstraction levels, from knowledge bases and system architecture, to software source code and detailed hardware design. The Action contributes to the construction of Rich-Model Toolkit, a new unified infrastructure that precisely defines the meaning of Rich Models, introduces standardized representation formats, and incorporates a number of automated reasoning tools. Moreover, the Action develops and deploys new tools for automated reasoning that communicate using these standardized formats. The resulting tools will have a wide range of applicability and improved efficiency, helping system developers construct reliable systems through automated reasoning, analysis, and synthesis.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , team leader
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Dudka Kamil, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Gach Marek, Ing. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Hýsek Jiří, Ing. (UITS FIT VUT)
Konečný Filip, Ing. (UITS FIT VUT)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Letko Zdeněk, Ing., Ph.D. (UITS FIT VUT)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
2012
- KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. FIT Monograph. Brno: Faculty of Information Technology BUT, 2012. ISBN 978-80-214-4464-5. Detail
- KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software. Lecture Notes in Computer Science, vol. 2012, no. 7186, pp. 177-192. ISSN 0302-9743. Detail
- KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science, vol. 2012, no. 7119, pp. 123-131. ISSN 0302-9743. Detail
- DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. Testing of Concurrent Programs with Genetic Algorithms. Lecture Notes in Computer Science, vol. 2012, no. 7515, pp. 152-167. ISSN 0302-9743. Detail
2011
- HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743. Detail
- HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. Detail
- DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Lecture Notes in Computer Science, vol. 2011, no. 6806, pp. 372-378. ISSN 0302-9743. Detail
- DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. 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. Detail
2010
- ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard and VOJNAR Tomáš. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174. Berlín: Springer Verlag, 2010, pp. 132-147. ISBN 978-3-642-14294-9. Detail
- ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang, MAYR Richard and 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. Lecture Notes in Computer Science, vol. 6015. Berlín: Springer Verlag, 2010, pp. 158-174. ISBN 978-3-642-12001-5. Detail
2011
- A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, software, 2011
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš Detail
2010
- Forester: A Tool for Verification of Programs with Pointers, software, 2010
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail - libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš Detail - Replay Tracer & BMC, software, 2010
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš Detail - Tool for verification of systems described using the Modechart formalism, software, 2010
Authors: Gach Marek, Fiedor Jan, Češka Milan Detail - Tool for verification of systems specified in RT-Logic language, software, 2010
Authors: Fiedor Jan, Gach Marek, Češka Milan Detail