Mgr. Lukáš Holík, Ph.D.

Advanced Formal Approaches in the Design and Verification of Computer-Based Systems

Czech title:Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů
Reseach leader:Češka Milan
Team leaders:Cerhák Michal, Erlebach Pavel, Holík Lukáš, Janoušek Vladimír, Kironský Elöd, Kočí Radek, Křena Bohuslav, Polášek Petr, Rogalewicz Adam, Smrčka Aleš, Vojnar Tomáš
Agency:Czech Science Foundation
Code:GA102/07/0322
Start:2007-01-01
End:2009-12-31
Keywords:formal models, simulation verification, formal verification, model checking
Annotation:
High-level design and formal verification are promising approaches for improving reliability and safety of computer systems. This project is proposed by the highly experienced team with the expressive results and the international cooperation with the prestigious research teams. The project aims to explore and use advanced formal approaches from the fields like system theory, logics, theoretical computer science, and artificial intelligence in the area of the high-level design and formal verification. We believe that these approaches can significantly improve the verification abilities, especially in the cases on which the brute-force approach does not succeed. The proposed research project covers complementary methods, i.e., the model-driven design, the simulation-based verification, and the model checking of finite-state as well as infinite-state systems. The research should result in developing new approaches and methods with unique properties. These methods will be validated by the prototype implementation and will be evaluated by suitable case studies.

Products

2009Clock Domain Crossing Analyzer, software, 2009
Authors: Smrčka Aleš
 FLATA, 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áš
2008Java Atomicity Violation Detector & Healer, software, 2008
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav
 Model checking Using Symbolic Execution, software, 2008
Authors: Křena Bohuslav, Braione Pietro, Denaro Giovanni, Pezze Mauro
 PNtalk, software, 2008
Authors: Kočí Radek
2007Java Race Detector & Healer, software, 2007
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav
 SmallDEVS-07, software, 2007
Authors: Janoušek Vladimír, Kironský Elöd

Publications

2010BOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Berlin: Springer Verlag, 2010, pp. 227-242. ISBN 978-3-642-14294-9.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Acta Informatica. 2010, vol. 47, no. 1, pp. 1-31. ISSN 0001-5903.
 KOČÍ Radek, JANOUŠEK Vladimír and ZBOŘIL František. Object Oriented Petri Nets - Modelling Techniques Case Study. International Journal of Simulation Systems, Science & Technology. 2010, vol. 10, no. 3, pp. 32-44. ISSN 1473-8031.
2009ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science. 2009, vol. 20, no. 4, pp. 685-700. ISSN 0129-0541.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno, 2009.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009). Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009, pp. 1-12. ISBN 978-3-939897-13-2.
 ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science. 2009, vol. 2009, no. 251, pp. 27-48. ISSN 1571-0661.
 BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009.
 BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7.
 DUDKA Vendula, KŘENA Bohuslav and VOJNAR Tomáš. Self-healing Assurance using Bounded Model Checking. In: Computer Aided Systems Theory - EUROCAST 2009. Berlin: Springer Verlag, 2009, pp. 295-303. ISBN 978-3-642-04771-8.
 DUDKA Vendula, VOJNAR Tomáš and KŘENA Bohuslav. Self-healing Assurance using Bounded Model Checking. In: Computer Aided Systems Theory. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2009, pp. 99-100. ISBN 978-84-691-8502-5.
 HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009.
 HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009, pp. 93-101. ISBN 978-3-939897-15-6.
 IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2009, pp. 165-177. ISBN 978-3-642-02978-3.
 JANOUŠEK Vladimír and KIRONSKÝ Elöd. Interactive evolutionary modelling and simulation of discrete-event systems using prototypical objects. International Journal of Autonomic Computing. London: Inderscience Publishers, 2009, vol. 1, no. 2, pp. 104-120. ISSN 1741-8569.
 JANOUŠEK Vladimír and KVĚTOŇOVÁ Šárka. On the Multilevel Petri Nets-Based Models in Project Engineering. In: International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009, pp. 173-188.
 KOČÍ Radek and JANOUŠEK Vladimír. On the Dynamic Features of PNtalk. In: International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009, pp. 189-206.
 KOČÍ Radek and JANOUŠEK Vladimír. Simulation Based Design of Control Systems Using DEVS and Petri Nets. In: Computer Aided Systems Theory - EUROCAST 2009. Berlin: Springer Verlag, 2009, pp. 849-856. ISBN 978-3-642-04771-8.
 KOČÍ Radek and JANOUŠEK Vladimír. Towards Simulation-Based Design of the Software Systems. In: The Fourth International Conference on Software Engineering Advances. Los Alamitos: IEEE Computer Society, 2009, pp. 452-457. ISBN 978-1-4244-4779-4.
 KŘENA Bohuslav, LETKO Zdeněk, NIR-BUCHBINDER Yarden, TZOREF-BRILL Rachel, UR Shmuel and VOJNAR Tomáš. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno, 2009.
 KŘENA Bohuslav, LETKO Zdeněk, NIR-BUCHBINDER Yarden, TZOREF-BRILL Rachel, UR Shmuel and VOJNAR Tomáš. A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing. In: Runtime Verification. Berlin: Springer Verlag, 2009, pp. 101-114. ISBN 978-3-642-04693-3.
 MAZAL Zdeněk, KOČÍ Radek, JANOUŠEK Vladimír and ZBOŘIL František. Modelling intelligent agents for autonomic computing in the PNagent framework. International Journal of Autonomic Computing. London: Inderscience Publishers, 2009, vol. 1, no. 2, pp. 121-139. ISSN 1741-8569.
2008ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno, 2008.
 ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno, 2008.
 ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2008, pp. 212-222. ISBN 978-3-540-70843-8.
 ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Computing Simulations over Tree Automata (Efficient Techniques for Reducing Tree Automata). In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Verlag, 2008, pp. 93-108. ISBN 978-3-540-78799-0.
 ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno, 2008.
 ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2008, pp. 3-11. ISBN 978-80-7355-082-0.
 BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods in System Design. Berlin: Springer Verlag, 2008, vol. 32, no. 2, pp. 129-172. ISSN 0925-9856.
 BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
 BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2008, pp. 57-67. ISBN 978-3-540-70843-8.
 DUDKA Vendula. Bounded Model Checking Using Java PathFinder. In: Proceedings of the 14th Conference STUDENT EEICT 2008. Brno: Brno University of Technology, 2008, pp. 247-249. ISBN 978-80-214-3615-2.
 HABERMEHL Peter and VOJNAR Tomáš, ed. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Faculty of Information Technology BUT, 2008. ISBN 978-80-214-3697-8.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Berlin: Springer Verlag, 2008, pp. 558-573. ISBN 978-3-540-89438-4.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. What else is decidable about integer arrays?. In: Foundations of Software Science and Computation Structures. Berlin: Springer Verlag, 2008, pp. 475-490. ISBN 978-3-540-78497-5.
 HÝSEK Jiří. Visual design of SmallDEVS models using statecharts. In: Proceedings of ASIS 2008. Rožnov pod Radhoštěm: Czech Science Foundation, 2008, p. 6. ISBN 978-80-86840-42-0.
 JANOUŠEK Vladimír and KIRONSKÝ Elöd. Reflective Framework for Interactive Modeling and Simulation of Intelligent Systems. In: Proceedings of Nineteenth International Conference on Systems Engineering 19-21 August 2008 Las Vegas, Nevada. Los Alamitos: IEEE Computer Society, 2008, pp. 480-485. ISBN 978-0-7695-3331-5.
 JANOUŠEK Vladimír and KOČÍ Radek. The PNtalk/SmallDEVS Framework -- Meta-level Modeling Techniques. In: Proceedings of CSE 2008 International Scientific Conference on Computer Science and Engineering. Košice: elfa, s.r.o., TU Kosice, 2008, pp. 16-23. ISBN 978-80-8086-092-9.
 JANOUŠEK Vladimír, KOČÍ Radek, MAZAL Zdeněk and ZBOŘIL František. PNagent: a Framework for Modelling BDI Agents using Object Oriented Petri Nets. In: Proceedings of 8th ISDA. Los Alamitos: IEEE Computer Society, 2008, pp. 420-425. ISBN 978-0-7695-3382-7.
 KOČÍ Radek and JANOUŠEK Vladimír. System Design with Object Oriented Petri Nets Formalism. In: The Third International Conference on Software Engineering Advances Proceedings ICSEA 2008. Los Alamitos: IEEE Computer Society, 2008, pp. 421-426. ISBN 978-0-7695-3372-8.
 KOČÍ Radek, JANOUŠEK Vladimír and ZBOŘIL František. Object Oriented Petri Nets -- Modelling Techniques Case Study. In: Second UKSIM European Symposium on Computer Modeling and Simulation. Liverpool: IEEE Computer Society, 2008, pp. 165-170. ISBN 978-0-7695-3325-4.
 LETKO Zdeněk, VOJNAR Tomáš and KŘENA Bohuslav. AtomRace: data race and atomicity violation detector and healer. In: PADTAD '08. Seattle: Association for Computing Machinery, 2008, pp. 1-10. ISBN 978-1-60558-052-4.
 LETKO Zdeněk. An Architecture for Self-Healing of Data Races and Atomicity Violations for Java. In: Proceedings of the 14th Conference STUDENT EEICT 2008. Brno: Brno University of Technology, 2008, pp. 256-258. ISBN 978-80-214-3615-2.
 MAZAL Zdeněk, JANOUŠEK Vladimír and KOČÍ Radek. Enhancing the PNtalk Language with Negative Predicates. In: MOSIS '08. Ostrava, 2008, pp. 28-34. ISBN 978-80-86840-40-6.
 NOVOSAD Petr and ČEŠKA Milan. Algorithms for Computing Coverability Graphs for Continuous Petri Nets. In: Proceedings of 22th European Simulation and Modelling Conference ESM'2008. Le Havre: EUROSIM-FRANCOSIM-ARGESIM, 2008, pp. 489-491. ISBN 978-90-77381-44-1.
 NOVOSAD Petr and ČEŠKA Milan. Algorithms for Computing Coverability Graphs for Hybrid Petri Nets. In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2008, pp. 177-183. ISBN 978-80-7355-082-0.
 POLÁŠEK Petr and JANOUŠEK Vladimír. Modeling and Simulation Management in Distributed Environment Using Web Services. In: Proceedings of the 14th International Congress of Cybernetics and Systems of WOCS. Wroclaw: Wroclaw University of Technology, 2008, p. 9. ISBN 978-83-7493-400-8.
 SKLENÁŘ Jaroslav, CUTARAJ Valerie and ČEŠKA Milan. Using Integer Programming for Discrete Problem Optimization. In: The 2008 European Simulation and Modelling Conference. LE HAVRE: EUROSIM-FRANCOSIM-ARGESIM, 2008, pp. 19-21. ISBN 978-90-77381-44-1.
 VOJNAR Tomáš, ČEŠKA Milan, ROGALEWICZ Adam, ERLEBACH Pavel, HOLÍK Lukáš, BOUAJJANI Ahmed, HABERMEHL Peter, TOUILI Tayssir and MORO Pierre. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií. 2008, vol. 2008, no. 1, pp. 21-22. ISSN 1210-4612.
2007DUDKA Vendula, KŘENA Bohuslav and VOJNAR Tomáš. Using JavaPathFinder for Self-healing Assurance. In: Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007. Znojmo: Ing. Zdeněk Novotný, CSc., 2007, pp. 67-73. ISBN 978-80-7355-077-6.
 HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Berlin: Springer Verlag, 2007, pp. 145-161. ISBN 978-3-540-75595-1.
 JANOUŠEK Vladimír and KOČÍ Radek. Embedding Object-Oriented Petri Nets into a DEVS-based Simulation Framework. In: Proceedings of the 16th International Conference on System Science. Wroclaw: Wroclaw University of Technology, 2007, pp. 386-395. ISBN 978-83-7493-339-1.
 JANOUŠEK Vladimír and KOČÍ Radek. Simulation and Design of Systems with Object Oriented Petri Nets. In: Proceedings of the 6th EUROSIM Congress on Modelling and Simulation. Ljubljana: ARGE Simulation News, 2007, p. 9. ISBN 978-3-901608-32-2.
 JANOUŠEK Vladimír, KIRONSKÝ Elöd and POLÁŠEK Petr. An Architecture for Simulation-Based Evolutionary Design of Systems. In: Proceedings of the 16th International Conference on System Science. Wroclaw: Wroclaw University of Technology, 2007, pp. 396-405. ISBN 978-83-7493-339-1.
 KOČÍ Radek, MAZAL Zdeněk, ZBOŘIL František and JANOUŠEK Vladimír. Modeling Deliberative Agents Using Object Oriented Petri Nets. In: Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007, pp. 15-20. ISBN 0-7695-2976-3.
 KŘENA Bohuslav, LETKO Zdeněk, TZOREF-BRILL Rachel, UR Shmuel and VOJNAR Tomáš. Healing Data Races On-The-Fly. In: Proceedings of 5th International Workshop on Parallel and Distributed Systems: Testing and Debugging Modelling - PADTAD'07. London: Association for Computing Machinery, 2007, pp. 54-64. ISBN 978-1-59593-734-6.
 VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6.
 VOJNAR Tomáš. Stromové automaty s omezeními v symbolické verifikaci programů manipulujících vyvážené stromy. Současné trendy teoretické informatiky. Praha, 2007.
 ZBOŘIL František and KOČÍ Radek. Intention Structures Modelling Using Object Oriented Petri Nets. In: Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007, pp. 33-38. ISBN 0-7695-2976-3.
 ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing. London: Springer London, 2007, vol. 19, no. 3, pp. 363-374. ISSN 0934-5043.
 ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-Based Verification for Trees. In: Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2007, pp. 181-182. ISBN 978-3-540-75866-2.
 ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-based Verification for Trees. In: Computer Aided Systems Theory. Berlin: Springer Verlag, 2007, pp. 488-496. ISBN 978-3-540-75866-2.

Your IPv4 address: 54.91.171.137
Switch to IPv6 connection

DNSSEC [dnssec]