Prof. Ing. Tomáš Vojnar, Ph.D.

Rich-Model Toolkit -- An Infrastructure for Reliable Computer Systems

Czech title:Bohatý modelovací jazyk -- infrastruktura pro spolehlivé počítačové systémy
Reseach leader:Kuncak Viktor (EPFL)
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, European Cooperation in Science and Technology
Code:IC0901
Start:2009-10-30
End:2013-10-30
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

2011A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, software, 2011
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš
2010Forester: A Tool for Verification of Programs with Pointers, software, 2010
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš
 libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš
 Replay Tracer & BMC, software, 2010
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš
 Tool for verification of systems described using the Modechart formalism, software, 2010
Authors: Gach Marek, Fiedor Jan, Češka Milan
 Tool for verification of systems specified in RT-Logic language, software, 2010
Authors: Fiedor Jan, Gach Marek, Češka Milan
2009FLATA, software, 2009
Authors: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu
 Tool for Computing Simulations, software, 2009
Authors: Holík Lukáš, Šimáček Jiří, Vojnar Tomáš

Publications

2012DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. Testing of Concurrent Programs with Genetic Algorithms. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7515, pp. 152-167. ISSN 0302-9743.
 KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. Brno: Faculty of Information Technology BUT, 2012. ISBN 978-80-214-4464-5.
 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. 2012, vol. 2012, no. 7186, pp. 177-192. ISSN 0302-9743.
 KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7119, pp. 123-131. ISSN 0302-9743.
2011DUDKA 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.
 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. 2011, vol. 2011, no. 6806, pp. 372-378. ISSN 0302-9743.
 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.
 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. 2011, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743.
2010ABDULLA 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. Berlín: Springer Verlag, 2010, pp. 132-147. ISBN 978-3-642-14294-9.
 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. Berlín: Springer Verlag, 2010, pp. 158-174. ISBN 978-3-642-12001-5.

Your IPv4 address: 54.91.171.137
Switch to IPv6 connection

DNSSEC [dnssec]