Prof. RNDr. Milan Češka, CSc.
|
| Reseach leader: | Kuncak Viktor |
|---|
| Team leaders: | Vojnar Tomáš |
|---|
| Team members: | Češka Milan, Dudka Kamil, Fiedor Jan, Gach Marek, Holík Lukáš, Hýsek Jiří, Konečný Filip, Křena Bohuslav, Letko Zdeněk, Peringer Petr, Rogalewicz Adam, Smrčka Aleš, Šimáček Jiří |
|---|
| Agency: | COST |
| Code: | IC0901 |
| Start: | 2009 |
| End: | 2013 |
| Keywords: | formal modelling, formal verification, decision procedures, synthesis
|
| Annotation: |
|---|
| 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. |
Products
|
Publications
| 2012 | Hrubá Vendula, Křena Bohuslav, Letko Zdeněk, Ur Shmuel, Vojnar Tomáš: Testing of Concurrent Programs with Genetic Algorithms, In: Lecture Notes in Computer Science, Vol. 2012, No. 7515, DE, p. 152-167, ISSN 0302-9743 |
| | Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Analysis and Testing of Concurrent Programs, Brno, CZ, FIT VUT, 2012, p. 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, Vol. 2012, No. 7186, DE, p. 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, Vol. 2012, No. 7119, DE, p. 123-131, ISSN 0302-9743 |
| 2011 | 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, Vol. 2011, No. 6806, DE, p. 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, p. 23 |
| | 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, Vol. 2011, No. 6806, DE, p. 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, p. 30 |
| 2010 | 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, p. 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), In: Tools and Algorithms for the Construction and Analysis of Systems, Berlín, DE, Springer, 2010, p. 158-174, ISBN 978-3-642-12001-5 |
|
|
Faculty of Information Technology
![[dnssec]](/common/img/dnssec.png)