Tomáš Vojnar

Publications at DBLP.
Publications at Google Scholar.

2021 

• V. Malik and T. Vojnar. Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects. In Proc. of the IEEE International Conference on Software Testing, Verification and Validation 2021---ICST'21, Ipojuca, Brazil, virtual due to COVID-19. To be published by IEEE, 2021. A preliminary version is available here. The DiffKemp tool is available here.
• V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Automata Terms in a Lazy WSkS Decision Procedure. Journal of Automated Reasoning, 65(7):971--999, 2021. The first version appeared in the the Proc. of CADE-27.
• L. Charvat, A. Smrcka, and T. Vojnar. Utilizing Parametric Systems for Detection of Pipeline Hazards. International Journal on Software Tools for Technology Transfer (STTT), XX(XX):XXX--XXX, Springer, XXXX. A preliminary version is available here.

2020 

• L. Turonova, L. Holik, O. Lengal, O. Saarikivi, M. Veanes, and T. Vojnar. Regex Matching with Counting-Set Automata. In Proc. of the OOPSLA'20 conference, Chicago, USA, virtual due to COVID-19. Proceedings of the ACM on Programming Languages, 4(OOPSLA):218:1--218:30, ACM, 2020. A video presentation is available here. An extended version is available as the MSR-TR-2020-31 technical report, Microsoft Research, 2020.
• M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. Adaptive Verifiability-driven Strategy for Evolutionary Approximation of Arithmetic Circuits. Applied Soft Computing, 95(106466), Elsevier, 2020.
• V. Havlena, L. Holik, O. Lengal, O. Vales, and T. Vojnar. Antiprenexing for WSkS: A Little Goes a Long Way. In Proc. of 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning---LPAR-23, Alicante, Spain (cancelled due to COVID-19), volume 73 of EPiC Series in Computing, pages 298--316, 2020.
• M. Ceska, J. Matyas, V. Mrazek, and T. Vojnar. Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits. In Proc. of 23rd International Conference on Theory and Applications of Satisfiability Testing---SAT'20, virtual due to COVID-19, volume 12178 of LNCS, pages 481--491, 2020. Springer-Verlag.
• P. Peringer, V. Sokova, and T. Vojnar. PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation. In Proc. of 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems--- as a competition contribution within the 9th International Competition on Software Verification---SV-COMP'20, Dublin, Ireland (cancelled due to COVID-19), volume 12079 of LNCS, pages 408--412, 2020. Springer-Verlag. The Predator tool is available here.
• V. Malik, P. Schrammel, and T. Vojnar. 2LS: Heap Analysis and Memory Safety. In Proc. of 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems--- as a competition contribution within the 9th International Competition on Software Verification---SV-COMP'20, Dublin, Ireland (cancelled due to COVID-19), volume 12079 of LNCS, pages 368--372, 2020. Springer-Verlag. The 2LS tool is available here.
• M. Chalupa, T. Jasek, L. Tomovic, M. Hruska, V. Sokova, P. Ayaziova, J. Strejcek, and T. Vojnar. Symbiotic 7: Integration of Predator and More. In Proc. of 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems--- as a competition contribution within the 9th International Competition on Software Verification---SV-COMP'20, Dublin, Ireland (cancelled due to COVID-19), volume 12079 of LNCS, pages 413--417, 2020. Springer-Verlag. The Symbiotic tool is available here.
• L. Holik, R. Iosif, A. Rogalewicz, and T. Vojnar. Abstraction Refinement for Trace Inclusion of Infinite State Systems. Formal Methods in System Design, 55(3):137--170, Springer, 2020. An extended abstract appeared in the the Proc. of TACAS'16. A preliminary version is available at arXiv with the id 1410.5056. A prototype implementation is available in the tool called INCLUDER (tracer).
• M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar.  Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection.  International Journal on Software Tools for Technology Transfer (STTT), 22(5):523--539, Springer, 2020. An extended abstract appeared in the the Proc. of TACAS'18. A preliminary version is available here.

2019 

• L. Holik, O. Lengal, O. Saarikivi, L. Turonova, M. Veanes, and T. Vojnar. Succinct Determinisation of Counting Automata via Sphere Construction. In Proc. of 17th Asian Symposium on Programming Languages and Systems---APLAS'19, Bali, Indonesia, volume 11893 of LNCS, pages 468--489, 2019. Springer-Verlag. A preliminary version is available here.
• Y.-F. Chen, C.-Y. Chiang, L. Holik, W.-T. Kao, H.-H. Lin, T. Vojnar, Y.-F. Wen, and W.-C. Wu. J-ReCoVer: Java Reducer Commutativity Verifier. In Proc. of 17th Asian Symposium on Programming Languages and Systems---APLAS'19, Bali, Indonesia, volume 11893 of LNCS, pages 357--366, 2019. Springer-Verlag. A preliminary version is available here. The J-ReCoVer tool is available here.
• V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Automata Terms in a Lazy WSkS Decision Procedure. In Proc. of the 27th International Conference on Automated Deduction---CADE-27, Natal, Brazil, volume 11716 of LNCS, pages 300--318, 2019. Springer-Verlag. The best paper award of CADE-27. An extended version appeared as the technical report CoRR abs/1905.08697, 2019.
• M. Ceska, V. Havlena, L. Holik, J. Korenek, O. Lengal, D. Matousek, J. Matousek, J. Semric, and T. Vojnar. Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. In Proc. of 27th IEEE International Symposium On Field-Programmable Custom Computing Machines---FCCM'19, San Diego, USA, pages 109--117, 2019. IEEE. An extended version appeared as the technical report CoRR abs/1904.10786, 2019.
• M. Ceska jr., M. Ceska, J. Matyas, A. Pankuch, and T. Vojnar. Approximating Complex Arithmetic Circuits with Guaranteed Worst-Case Relative Error. In Proc. of the 17th International Conference on Computer Aided Systems Theory---EUROCAST'19, Las Palmas, Spain, volume 12013 of LNCS, pages 482--490, 2019. Springer-Verlag. A preliminary version is available here.
• V. Malik, M. Hruska, P. Schrammel, and T. Vojnar. 2LS: Heap Analysis and Memory Safety (Competition Contribution). Technical report CoRR abs/1903.00712 related to the SV-COMP'19 competition, 2019. The 2LS tool is available here.
• T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. Acta Informatica, 56(3):205--228, Springer, 2019. An extended abstract appeared in the the Proc. of TACAS'15. A preliminary version is available here. The concerned tool called dWiNA is available here.

2018 

• V. Malik, M. Hruska, P. Schrammel, and T. Vojnar. Template-Based Verification of Heap-Manipulating Programs. In Proc. of 18th International Conference on Formal Methods in Computer-Aided Design---FMCAD'18, Austin, USA, 2018. IEEE. A preliminary version is available here. The 2LS tool is available here.
• L. Holik, O. Lengal, J. Sic, M. Veanes, and T. Vojnar. Simulation Algorithms for Symbolic Automata. In Proc. of 16th International Symposium on Automated Technology for Verification and Analysis---ATVA'18, Los Angeles, USA, volume 11138 of LNCS, pages 109--125, 2018. Springer-Verlag. An extended version appeared as the technical report CoRR abs/1807.08487, 2018.
• J. Fiedor, M. Muzikovska, A. Smrcka, O. Vasicek, and T. Vojnar. Advances in the ANaConDA Framework for Dynamic Analysis and Testing of Concurrent C/C++ Programs. In Proc. of 27th International Symposium on Software Testing and Analysis---ISSTA'18, Amsterdam, Netherlands, pages 356--359, 2018. ACM. The best tool demo award of ISSTA'18. A preliminary version is available here. The ANaConDA tool is available here.
• M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. ADAC: Automated Design of Approximate Circuits. In Proc. of 30th International Conference on Computer Aided Verification---CAV'18, Oxford, UK, volume 10981 of LNCS, pages 612--620, 2018. Springer-Verlag. The ADAC tool is available here.
• M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proc. of 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'18, Thessaloniki, Greece, volume 10806 of LNCS, pages 155--175, 2018. Springer-Verlag. An extended version appeared as the technical report CoRR abs/1710.08647, 2018.
• V. Malik, S. Marticek, P. Schrammel, M.K. Srivas, T. Vojnar, and J. Wahlang. 2LS: Memory Safety and Non-termination (Competition Contribution). In Proc. of 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'18, Thessaloniki, Greece, volume 10806 of LNCS, pages 417--421, 2018. Springer-Verlag. The 2LS tool is available here.
• T. Fiedor, L. Holik, A. Rogalewicz, M. Sinn, T. Vojnar, and F. Zuleger. From Shapes to Amortized Complexity. In Proc. of 19th International Conference on Verification, Model Checking, and Abstract Interpretation---VMCAI'18, Los Angeles, CA, USA, volume 10747 of LNCS, pages 205--225, 2018. Springer-Verlag. A preliminary version is available here.
• L. Holik, A.W. Lin, P. Janku, P. Ruemmer, and T. Vojnar. String Constraints with Concatenation and Transducers Solved Efficiently. In Proc. of 45th ACM SIGPLAN Symposium on Principles of Programming Languages---POPL'18, Los Angeles, CA, USA, 2018. Proceedings of the ACM on Programming Languages, Vol. 2, Article 4. ACM. A preliminary version is available here. The SLOTH string solver implemented within the paper is available here.
• J.M. Lourenco, J. Fiedor, B. Krena, and T. Vojnar. Discovering Concurrency Errors. A chapter of Lectures on Runtime Verification, volume 10457 of LNCS, pages 34--60, 2018. Springer-Verlag. A preliminary version is available here.

2017 

• M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In Proc. of 36th International Conference On Computer Aided Design---ICCAD'17, Irvine, CA, USA, pages 416--423, 2017. IEEE CS. A bronze medal in the 2018 Human-Competitive Awards: "Humies". A preliminary version is available here.
• L. Holik, R. Meyer, T. Vojnar, and S. Wolff. Effect Summaries for Thread-Modular Analysis (Sound Analysis Despite an Unsound Heuristic). In Proc. of 24th Static Analysis Symposium---SAS'17, New York City, NY, USA, volume 10422 of LNCS, pages 169--191, 2017. Springer-Verlag. An extended version appeared as the technical report CoRR abs/1705.03701, 2017. The implementation is available here.
• R. Avros, V. Dudka, B. Krena, Z. Letko, H. Pluhackova, S. Ur, T. Vojnar, and Z. Volkovitch. Boosted Decision Trees for Behaviour Mining of Concurrent Programmes. Concurrency and Computation: Practice and Experience, 29(21), pp. 21, Wiley, 2017. An extended abstract appeared in the the Proc. of MEMICS'14. A preliminary version is available here.
• R.J. Dias, C. Ferreira, J. Fiedor, J.M. Lourenco, A. Smrcka, D.G. Sousa, and T. Vojnar. Verifying Concurrent Programs Using Contracts. In Proc. of 10th IEEE International Conference on Software Testing, Verification and Validation---ICST'17, Waseda University, Tokyo, Japan, pages 196--206, 2017. IEEE. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2016-02, FIT BUT, 2016. The slides from the presentation are available here. The concerned ANaConDA framework is available here.
• B. Krena, H. Pluhackova, S. Ur, and T. Vojnar. Prediction of Coverage of Expensive Concurrency Metrics Using Cheaper Metrics. In Proc. of 16th International Conference on Computer Aided Systems Theory---EUROCAST'17, Las Palmas, Spain, volume 10672 of LNCS, pages 99--108, 2018. Springer-Verlag. A preliminary version is available here.
• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design, 51(3):575--607, Springer-Verlag, 2017. An extended abstract appeared in the the Proc. of APLAS'14. A preliminary version is available here. The concerned tool called SPEN is available here.
• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. SPEN: A Solver for Separation Logic. In Proc. of 9th NASA Formal Methods Symposium---NFM'17, NASA Ames Research Center, Moffett Field, CA, USA, volume 10227 of LNCS, pages 302--309, 2017. Springer-Verlag. A preliminary version is available here. The SPEN tool is available here.
• T. Fiedor, L. Holik, P. Janku, O. Lengal, and T. Vojnar. Lazy Automata Techniques for WS1S. In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'17, Uppsala, Sweden, volume 10205 of LNCS, pages 407--425, 2017. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1701.06282, 2017. The slides from the presentation are available here. The concerned tool Gaston is available here.
• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Forester: From Heap Shapes to Automata Predicates (Competition Contribution). In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'17, Uppsala, Sweden, volume 10206 of LNCS, pages 365--369, 2017. Springer-Verlag. A preliminary version is available here. The Forester tool is available here.
• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, and T. Vojnar. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proc. of 18th International Conference on Verification, Model Checking, and Abstract Interpretation---VMCAI'17, Paris, France, volume 10145 of LNCS, pages 288--309, 2017. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2016-03, FIT BUT, Brno, Czech Republic, 2016. The Forester tool is available here.

2016 

• R. Iosif, A. Rogalewicz, and T. Vojnar. Abstraction Refinement for Trace Inclusion of Infinite State Systems . In Proc of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'16, Eindhoven, Netherlands, volume of LNCS 9636, pages 71--89, 2016. Springer-Verlag. A preliminary version is available at arXiv with the id 1410.5056. A prototype implementation is available in the tool called INCLUDER (tracer).
• L. Holik, M. Kotoun, P. Peringer, V. Sokova, M. Trtik, and T. Vojnar. Predator Shape Analysis Tool Suite . In Proc. of 12th Haifa Verification Conference---HVC'16, Haifa, Israel, volume 10028 of LNCS, pages 202--209, 2016. Springer-Verlag. A preliminary version is available here. The Predator tool suite is available here.
• L. Charvat, A. Smrcka, and T. Vojnar. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems . In Proc. of 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'16, Telc, Czech republic, volume 233 of EPTCS, pages 87--93, 2016. The Hades tool is available here.
• M. Kotoun, P. Peringer, V. Sokova, and T. Vojnar. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'16 as a competition contribution within the 5th International Competition on Software Verification---SV-COMP'16, London, UK, volume 9636 of LNCS, pages 942--945, 2016. Springer-Verlag. A preliminary version is available here.
• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Run Forester, Run Backwards! (Competition Contribution). In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'16 as a competition contribution within the 5th International Competition on Software Verification---SV-COMP'16, London, UK, volume 9636 of LNCS, pages 923--926, 2016. Springer-Verlag. A preliminary version is available here.
• K. Dudka, L. Holik, P. Peringer, M. Trtik, and T. Vojnar. From Low-Level Pointers to High-Level Containers . In Proc of 17th International Conference on Verification, Model Checking, and Abstract Interpretation---VMCAI'16, St. Petersburg, Florida, USA, volume of LNCS 9583, pages 431--452,2016. Springer-Verlag. A preliminary version is available at arXiv with the id 1510.07995. The prototype implementation Predator-adt is available here.
• P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Acta Informatica, 53(4):357--385, Springer-Verlag, 2016. An extended abstract appeared in the the Proc. of ATVA'13. A preliminary version is available here.

2015 

• T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'15, London, UK, volume 9035 of LNCS, pages 658--674, 2015. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2014-01, FIT BUT, Brno, Czech Republic, 2014. The concerned tool called dWiNA is available here.
• P. Muller, P. Peringer, and T. Vojnar. Predator Hunting Party (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'15 as a competition contribution within the 4th International Competition on Software Verification---SV-COMP'15, London, UK, volume 9035 of LNCS, pages 443--446, 2015. Springer-Verlag. A preliminary version is available here.
• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'15 as a competition contribution within the 4th International Competition on Software Verification---SV-COMP'15, London, UK, volume 9035 of LNCS, pages 432--435, 2015. Springer-Verlag. A preliminary version is available here.
• J. Fiedor, Z. Letko, J. Lourenco, and T. Vojnar. Dynamic Validation of Contracts in Concurrent Code. In Proc. of 15th International Conference on Computer Aided Systems Theory---EUROCAST'15, Las Palmas, Spain, volume 9520 of LNCS, pages 555-564, 2015. Springer-Verlag. A preliminary version is available here.
• L. Charvat, A. Smrcka, and T. Vojnar. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In Proc. of 15th International Conference on Computer Aided Systems Theory---EUROCAST'15, Las Palmas, Spain, volume 9520 of LNCS, pages 605--614, 2015. Springer-Verlag. A preliminary version is available here.
• J. Fiedor, V. Hruba, B. Krena, Z. Letko, S. Ur, and T. Vojnar. Advances in Noise-based Testing of Concurrent Software. In Software Testing, Verification and Reliability, 25(3):272--309, Elsevier, 2015. A preliminary version is available here.

2014 

• L. Charvat, A. Smrcka, and T. Vojnar. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In Proc. of 15th International Workshop on Microprocessor Test and Verification---MTV'14, Austin, USA, IEEE CS, pages 83--89, 2014. A preliminary version is available here.
• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. In Proc. of 12th Asian Symposium on Programming Languages and Systems---APLAS'14, Singapore, 2014, volume 8858 of LNCS, pages 314--333, 2014. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2014-01, FIT BUT, Brno, Czech Republic, 2014. The concerned tool called SPEN is available here. Results of SPEN participating in the separation logic competition within SMT-COMP 2014 can be found here.
• R. Iosif, A. Rogalewicz, and T. Vojnar. Deciding Entailments in Inductive Separation Logic with Tree Automata. In Proc. of 12th International Symposium on Automated Technology for Verification and Analysis---ATVA'14, Sydney, Australia, 2014, volume 8837 of LNCS, pages 201--218, 2014. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1402.2127, arxiv.org, 2014. The concerned tool called SLIDE is available here. Results of SLIDE participating in the separation logic competition within SMT-COMP 2014 can be found here.
• V. Hruba, B. Krena, Z. Letko, H. Pluhackova, and T. Vojnar. Multi-objective Genetic Optimization for Noise-Based Testing of Concurrent Software. In Proc. of 6th Symposium on Search Based Software Engineering---SSBSE'14, Fortaleza, Brazil, volume 8636 of LNCS, pages 107--122, 2014. Springer-Verlag. A preliminary version is available here.
• J. Fiedor, Z. Letko, J. Lourenco, and T. Vojnar. On Monitoring C/C++ Transactional Memory Programs. In Proc. of 9th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'14, Telc, Czech Republic, volume 8934 of LNCS, pages 73--87, 2014. Springer-Verlag. A preliminary version is available here. The concerned tool called ANaConDA is available here.
• R. Avros, V. Hruba, B. Krena, Z. Letko, H. Pluhackova, S. Ur, T. Vojnar, and Z. Volkovitch. Boosted Decision Trees for Behaviour Mining of Concurrent Programs. In Proc. of 9th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'14, Telc, Czech Republic, pages 15--27, 2014. Novpress.
• K. Dudka, P. Peringer, and T. Vojnar. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'14 as a competition contribution within the 3rd International Competition on Software Verification---SV-COMP'14, Grenoble, France, volume 8413 of LNCS, pages 412--414, 2014. Springer-Verlag. A preliminary version is available here.
• P. Muller and T. Vojnar. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'14 as a competition contribution within the 3rd International Competition on Software Verification---SV-COMP'14, Grenoble, France, volume 8413 of LNCS, pages 395--397, 2014. Springer-Verlag. A preliminary version is available here.
• P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar. Mediating for Reduction (On Minimizing Alternating Büchi Automata). In Theoretical Computer Science, 552:26--43, Elsevier, 2014. A preliminary version is available here. An extended abstract appeared in the proceedings of FSTTCS'09.

2013 

• L. Holik, O. Lengal, J. Simacek, A. Rogalewicz, and T. Vojnar. Fully Automated Shape Analysis Based on Forest Automata. In Proc. of 25th International Conference on Computer Aided Verification---CAV'13, Saint Petersburg, Russia, volume 8044 of LNCS, pages 740--755, 2013. Springer-Verlag. A preliminary version is available here. The concerned tool called Forester is available here.
• P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In Proc. of 11th International Symposium on Automated Technology for Verification and Analysis---ATVA'13, Hanoi, Vietnam, volume 8172 of LNCS, pages 224--239, 2013. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2013-02, FIT BUT, Brno, Czech Republic, 2013.
• K. Dudka, P. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. In Proc. of 20th Static Analysis Symposium---SAS'13, Seattle, USA, volume 7935 of LNCS, pages 215--237, 2013. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2012-04, FIT BUT, Brno, Czech Republic, 2012. The concerned tool called Predator is available here.
• K. Dudka, P. Muller, P. Peringer, and T. Vojnar. Predator: A Tool for Verification of Low-level List Manipulation (Competition Contribution). In Proc. of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'13 as a competition contribution within the 2nd International Competition on Software Verification---SV-COMP'13, Rome, Italy, volume 7795 of LNCS, pages 627--629, 2013. Springer-Verlag. A preliminary version is available here.
• L. Charvat, A. Smrcka, and T. Vojnar. An Abstraction of Multi-port Memories with Arbitrary Addressable Units. In 14th International Conference on Computer Aided Systems Theory---EUROCAST'13, Las Palmas, Spain, volume 8111 of LNCS, pages 460--468, 2013. Springer-Verlag. A preliminary version is available here.
• P.A. Abdulla, J. Cederberg, and T. Vojnar. Monotonic Abstraction for Programs with Multiply-Linked Structures. In International Journal of Foundations of Computer Science, 24(2):187--210, World Scientific, 2013. A preliminary version appeared in the proceedings of RP'11.
• B. Krena and T. Vojnar. Automated Formal Analysis and Verification: An Overview. International Journal of General Systems, 42(4):335--365, Taylor and Francis, 2013. A preliminary version is available here.

2012 

• P. Habermehl, L. Holik, J. Simacek, A. Rogalewicz, and T. Vojnar. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design, 41(1):83--106, Springer-Verlag, 2012. An extended abstract appeared in the the Proc. of CAV'11. A preliminary version is available here.
• V. Hruba, B. Krena, Z. Letko, S. Ur, and T. Vojnar. Testing of Concurrent Programs Using Genetic Algorithms. In Proc. of 4th Symposium on Search Based Software Engineering---SSBSE'12, Riva del Garda, Trento, volume 7515 of LNCS, pages 152--167, 2012. Springer-Verlag. A preliminary version is available here.
• J. Fiedor and T. Vojnar. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. In Proc. of 3rd International Conference on Runtime Verification---RV'12, Istanbul, Turkey, 2012. volume 7687 of LNCS, pages 35--41, 2012. Springer-Verlag. A preliminary version is available here. The ANaConDA framework is available here. The best tool paper award of RV'12.
• J. Fiedor and T. Vojnar. Noise-based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In Proc. of 10th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging---PADTAD'12, Minneapolis, USA, pages 36--46, 2012. ACM Press. A preliminary version is available here.
• L. Charvat, A. Smrcka, and T. Vojnar. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In Proc. of 13th International Workshop on Microprocessor Test and Verification---MTV'12, Austin, USA, IEEE CS, 2012. A preliminary version is available here.
• O. Lengal, J. Simacek, and T. Vojnar. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'12, Talinn, Estonia, volume 7214 of LNCS, pages 79--94, 2012. Springer-Verlag. A preliminary version is available here.
• K. Dudka, P. Muller, P. Peringer, and T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution). In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'12 as a competition contribution within the 1st International Competition on Software Verification---SV-COMP'12, Talinn, Estonia, volume 7214 of LNCS, pages 545--548, 2012. Springer-Verlag. A preliminary version is available here.
• A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer (STTT), 14(2):167--191, Springer-Verlag, 2012. A preliminary version is available here.

2011 

• P. Habermehl, L. Holik, J. Simacek, A. Rogalewicz, and T. Vojnar. Forest Automata for Verification of Heap Manipulation. In Proc. of 23rd International Conference on Computer Aided Verification---CAV'11, Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 424--440, 2011. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2011-01, FIT BUT, Brno, Czech Republic, 2011. The concerned tool called Forester is available here.
• K. Dudka, P. Peringer, and T. Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In Proc. of 23rd International Conference on Computer Aided Verification---CAV'11, Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 372--378, 2011. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2011-02, FIT BUT, Brno, Czech Republic, 2011. The Predator tool is available here. A few slides presenting Predator are available here.
• L. Holik, O. Lengal, J. Simacek, and T. Vojnar. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. In Proc. of 9th International Symposium on Automated Technology for Verification and Analysis---ATVA'11, Taipei, Taiwan, volume 6996 of LNCS, pages 243--258, 2011. Springer-Verlag. More details and some post-ATVA extension of the approach can be found in the technical report FIT-TR-2011-04, FIT BUT, Brno, Czech Republic, 2011.
• B. Krena, Z. Letko, and T. Vojnar. Noise Injection Heuristics for Concurrency Testing. In Proc. of 7th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'11, Lednice, Czech Republic, volume 7119 of LNCS, pages 123--135, 2012. Springer-Verlag.
• B. Krena, Z. Letko, and T. Vojnar. Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software. In Proc. of 2nd International Conference on Runtime Verification---RV'11, San Francisco, CA, USA, volume 7186 of LNCS, pages 177--192, 2012. Springer-Verlag. A preliminary version is available here.
• J. Fiedor, V. Hruba, B. Krena, and T. Vojnar. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. In Proc. of 2nd International Conference on Runtime Verification---RV'11, San Francisco, CA, USA, volume 7186 of LNCS, pages 375--380, 2012. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2011-06, FIT BUT, Brno, Czech Republic, 2011. The DA-BMC tool is available here.
• P.A. Abdulla, Y.-F. Chen, L. Clemente, L. Holik, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Büchi Automata Inclusion Testing. In Proc. of 22nd International Conference on Concurrency Theory---CONCUR'11, Aachen, Germany, volume 6901 of LNCS, pages 187--202, 2011. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2011-03, FIT BUT, Brno, Czech Republic, 2011.
• P.A. Abdulla, J. Cederberg, and T. Vojnar. Monotonic Abstraction for Programs with Multiply-Linked Structures. In Proc. of 5th Workshop on Reachability Problems---RP'11, Genova, Italy, volume 6945 of LNCS, pages 125--138, 2011. Springer-Verlag.
• K. Dudka, P. Peringer, and T. Vojnar. An Easy to Use Infrastructure for Building Static Analysis Tools. In Proc. of 13th International Conference on Computer Aided Systems Theory---EUROCAST'11, Las Palmas, Spain, volume 6927 of LNCS, pages 527--534, 2012. Springer-Verlag. A preliminary version is available here. The described infrastructre is available here.
• J. Fiedor, Z. Letko, B. Krena, and T. Vojnar. A Uniform Classification of Common Concurrency Errors. In Proc. of 13th International Conference on Computer Aided Systems Theory---EUROCAST'11, Las Palmas, Spain, volume 6927 of LNCS, pages 519--526, 2012. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2010-03, FIT BUT, Brno, Czech Republic, 2010.
• A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with Lists are Counter Automata. Formal Methods in System Design, 38(2):158--192, Springer-Verlag, 2011. An extended abstract appeared in the Proc. of CAV'06.

2010 

• P.A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr, and T. Vojnar. When Simulation Meets Antichains (on Checking Language Inclusion of NFAs). In Proc. of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'10, Paphos, Cyprus, volume 6015 of LNCS (the ARCoSS subline), pages 158--174, 2010. Springer-Verlag. The EATCS best theory paper of ETAPS'10. An extended version appeared as the technical report FIT-TR-2010-01, FIT BUT, Brno, Czech Republic, 2010.
• P.A. Abdulla, Y.-F. Chen, L. Clemente, L. Holik, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. In Proc. of 22nd International Conference on Computer Aided Verification---CAV'10, Edinburgh, Scotland, volume 6174 of LNCS, pages 132--147, 2010. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2010-02, FIT BUT, Brno, Czech Republic, 2010.
• B. Krena, Z. Letko, S. Ur, and T. Vojnar. A Platform for Search-Based Testing of Concurrent Software. In Proc. of 8th International Workshop on Parallel and Distributed Systems: Testing and Debugging---PADTAD'10, Trento, Italy, pages 48--58, 2010. ACM Press.
• P. Habermehl, R. Iosif, and T. Vojnar. Automata-based Verification of Programs with Tree Updates. Acta Informatica, 47(1):1--31, 2010. Springer-Verlag. An extended version of a paper published originally at TACAS'06.

2009 

• P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar. Mediating for Reduction (On Minimizing Alternating Büchi Automata). In Proc. of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science---FSTTCS'09, Kanpur, India, volume 4 of LIPIcs, pages 1--12, 2009. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik. Also appeared as the technical report FIT-TR-2009-02, FIT BUT, Brno, Czech Republic, 2009.
• M. Bozga, P. Habermehl, R. Iosif, F. Konecny, and T. Vojnar. Automatic Verification of Integer Array Programs. In Proc. of 21st International Conference on Computer Aided Verification---CAV'09, Grenoble, France, volume 5643 of LNCS, pages 157--172, 2009. Springer-Verlag. An extended version appeared as the technical report TR-2009-2, Verimag, Grenoble, France, 2009.
• B. Krena, Z. Letko, Y. Nir-Buchbinder, R. Tzoref-Brill, S. Ur, and T. Vojnar. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. In Proc. of 9th International Workshop on Runtime Verification---RV'09, Grenoble, France, volume 5779 of LNCS, pages 101--114, 2009. Springer-Verlag. Also appeared as the technical report FIT-TR-2009-01, FIT BUT, Brno, Czech Republic, 2009.
• V. Hruba, B. Krena, and T. Vojnar. Self-Healing Assurance Using Bounded Model Checking. In Proc. of 12th International Conference on Computer Aided Systems Theory---EUROCAST'09, Las Palmas, Spain, volume 5717 of LNCS, pages 295--303, 2009. Springer-Verlag.
• P.A. Abdulla, L. Holik, L. Kaati, and T. Vojnar. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science, 251:27--48, 2009. An extended version of a paper published originally at MEMICS'08.
• P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, and T. Vojnar. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science, 20(4):685--700, 2009. An extended version of a paper published originally at CIAA'08.

2008 

• P. Habermehl, R. Iosif, and T. Vojnar. A Logic of Singly Indexed Arrays. In Proc. of 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning---LPAR'08, Doha, Qatar, volume 5330 of LNAI, pages 558--573, 2008. Springer-Verlag. An extended version appeared as the technical report TR-2008-9, Verimag, Grenoble, France, 2008.
• P.A. Abdulla, L. Holik, L. Kaati, and T. Vojnar. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. In Proc. of 4th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science---MEMICS'08, Znojmo, Czech Republic, pages 3--11, 2008. An extended version appeared as the technical report FIT-TR-2008-005, FIT BUT, Brno, Czech Republic, 2008.
• B. Krena, Z. Letko, and T. Vojnar. AtomRace: Data Race and Atomicity Violation Detector and Healer. In Proc. of 6th International Workshop on Parallel and Distributed Systems: Testing and Debugging---PADTAD'08, Seattle, WA, USA, pages 1--10, 2008. ACM Press.
• A. Bouajjani, P. Habermehl, L. Holik, T. Touili, and T. Vojnar. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In Proc. of 13th International Conference on Implementation and Application of Automata---CIAA'08, San Francisco, CA, USA, volume 5148 of LNCS, pages 57--67, 2008. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2008-001, FIT BUT, Brno, Czech Republic, 2008.
• P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, and T. Vojnar. Composed Bisimulation for Tree Automata. In Proc. of 13th International Conference on Implementation and Application of Automata---CIAA'08, San Francisco, CA, USA, volume 5148 of LNCS, pages 212--222, 2008. Springer-Verlag. The best paper award of CIAA'08. An extended version appeared as the technical report FIT-TR-2008-004, FIT BUT, Brno, Czech Republic, 2008.
• P. Habermehl, R. Iosif, and T. Vojnar. What else is decidable about integer arrays? In Proc. of 11th International Conference on Foundations of Software Science and Computation Structures---FoSSaCS'08, Budapest, Hungary, volume 4962 of LNCS, pages 475--490, 2008. Springer-Verlag. An extended version appeared as the technical report TR-2007-8, Verimag, Grenoble, France, 2007.
• P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, and T. Vojnar. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. In Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'08, Budapest, Hungary, volume 4963 of LNCS, pages 93--108, 2008. Springer-Verlag. An extended version appeared as the technical report FIT-TR-2007-001, FIT BUT, Brno, Czech Republic, 2007.
• A. Bouajjani, P. Habermehl, and T. Vojnar. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. Formal Methods in System Design, Springer-Verlag, 32(2):129--172, 2008. An extended abstract appeared in the Proc. of CONCUR'03.

2007 

• P. Habermehl, R. Iosif, A. Rogalewicz, and T. Vojnar. Proving Termination of Tree Manipulating Programs. In Proc. of 5th International Symposium on Automated Technology for Verification and Analysis---ATVA'07, Tokyo, Japan, volume 4762 of LNCS, pages 145--161, 2007. Springer-Verlag. An extended version appeared as the Verimag Technical Report TR-2007-1, Verimag, Grenoble, France, 2007.
• A. Smrcka and T. Vojnar. Verifying Parameterised Hardware Designs via Counter Automata. In Proc. of Haifa Verification Conference 2007---HVC'07, Haifa, Israel, 2007. Appeared in volume 4899 of LNCS, pages 51--68, 2008. Springer-Verlag.
• M. Ceska, P. Erlebach, and T. Vojnar. Generalized Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing, Springer-Verlag, 19(3):363--374, 2007.
• B. Krena, Z. Letko, R. Tzoref, S. Ur, and T. Vojnar. Healing Data Races On-The-Fly. In Proc. of 5th International Workshop on Parallel and Distributed Systems: Testing and Debugging---PADTAD'07, London, UK, 2007. ACM Press.
• M. Ceska, P. Erlebach, and T. Vojnar. Pattern-based Verification for Trees. In Proc. of 11th International Conference on Computer Aided Systems Theory---EUROCAST'07, Las Palmas, Spain, volume 4739 of LNCS, pages 488--496, 2007. Springer-Verlag.
• T. Vojnar. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Habilitation thesis, Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic, 2007. 189 p.

2006 

• A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In Proc. of 13th International Static Analysis Symposium---SAS'06, Seoul, Korea, volume 4134 of LNCS, pages 52--70, 2006. Springer-Verlag.
• A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with Lists are Counter Automata. In Proc of 18th International Conference on Computer Aided Verification---CAV'06, Seattle, WA, USA, volume 4144 of LNCS, pages 517--531, 2006. Springer-Verlag. An extended version appeared as the technical report TR-2006-3 of Verimag, Grenoble, France, 2006.
• P. Habermehl, R. Iosif, and T. Vojnar. Automata-based Verification of Programs with Tree Updates. In Proc. of 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'06, Vienna, Austria, volume 3920 of LNCS, pages 350--364, 2006. Springer-Verlag. An extended version appeared as the technical report TR-2005-16 of Verimag, Grenoble, France, 2005.
• A. Smrcka, V. Rehak, T. Vojnar, D. Safranek, P. Matousek, and Z. Rehak. Verifying VHDL Designs with Multiple Clocks in SMV. In Proc. of 11th International Workshop on Formal Methods for Industrial Critical Systems---FMICS'06, Bonn, Germany, volume 4346 of LNCS, pages 148--164, 2007. Springer-Verlag.
• M. Ceska, P. Erlebach, and T. Vojnar. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science, 145:113--130, 2006. Proc. of 5th International Workshop on Automated Verification of Critical Systems---AVOCS'05, Warwick, UK, pages 101--117, 2005.
• A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science, 149(1):37--48, 2006. Proc. of 7th International Workshop on Verification of Infinite-State Systems---Infinity'05, San Francisco, CA, USA, pages 15--24, 2005.

2005 

• A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Proc. of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'05, Edinburgh, UK, volume 3440 of LNCS, pages 13--29, 2005. Springer-Verlag.
• A. Smrcka, P. Matousek, and T. Vojnar. High-Level Modelling, Analysis, and Verification on FPGA-based Hardware Design. In Proc. of 13th International Conference on Correct Hardware Design and Verification Methods---Charme'05, Saarbrücken, Germany, volume 3725 of LNCS, pages 371--375, 2005. Springer-Verlag. An extended version appeared as the technical report 8/2005 of CESNET within the Liberouter project, Czech Republic, 2005.
• P. Erlebach and T. Vojnar. Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools. In Proc. of 8th International Conference on Information Systems Implementation and Modelling---ISIM'05, Hradec nad Moravici, Czech Republic, pages 219--226, 2005. MARQ Ostrava.
• M. Ceska, B. Krena, and T. Vojnar. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In Proc. of 10th International Conference on Computer Aided Systems Theory---EUROCAST'05, Las Palmas, Canary Islands, Spain, volume 3643 of LNCS, pages 275--280, 2005. Springer-Verlag.
• P. Hlavka, T. Kratochvila, V. Rehak, D. Safranek, P. Simecek, and T. Vojnar. CRC64 Algorithm Analysis and Verification. Technical report 27/2005 of CESNET within the Liberouter project, Czech Republic, 2005.
• P. Habermehl and T. Vojnar. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science, 138(3):21--36, 2005. Proc. of 6th International Workshop on Verification of Infinite-State Systems---Infinity'04, London, UK, 2004.

2004 

• A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. of 16th International Conference on Computer Aided Verification---CAV'04, Boston, Massachusetts, USA, volume 3114 of LNCS, pages 372--386, 2004. Springer-Verlag.
• A. Rogalewicz and T. Vojnar. Tree Automata In Modelling and Verification Of Concurrent Programs. In Proc. of ASIS'04, MARQ Ostrava, Czech Republic, pages 197--202, 2004.

2003 

• A. Bouajjani, P. Habermehl, and T. Vojnar. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. In Proc. of 14th International Conference on Concurrency Theory---CONCUR'03, Marseille, France, volume 2761 of LNCS, pages 174--190, 2003. Springer-Verlag.
• M. Ceska, L. Hasa, and T. Vojnar. Partial Order Reduction in Model Checking of Object-Oriented Petri Nets. In Proc. of 9th International Workshop on Computer Aided Systems Theory--EUROCAST'03, volume 2809 of LNCS, pages 265--278, 2003. Springer-Verlag.

2002 

• A. Bouajjani and T. Vojnar. Automata with Parameterized Arrays and Parameterized Networks of Automata. Research report D11 of the ADVANCE project (EU's 5th Framework IST FET project No. IST-1999-29082). LIAFA, University Paris 7, France, 2002.
• A. Bouajjani, P. Habermehl, and T. Vojnar. Verification of Parameterized Concurrent Systems with Resource Sharing. Research report D12.2 of the ADVANCE project EU's 5th Framework IST FET project No. IST-1999-29082). LIAFA, University Paris 7, France, 2002.
• M. Ceska, V. Janousek, and T. Vojnar. Modelling, Prototyping, and Verifying Concurrent and Distributed Applications Using Object-Oriented Petri Nets. Kybernetes: The International Journal of Systems & Cybernetics, 2002(9):1289--1299, 2002.

2001 

• T. Vojnar. Towards Formal Analysis and Verification over State Spaces of Object-Oriented Petri Nets. PhD thesis, Department of Computer Science and Engineering, FEECS, Brno University of Technology, Brno, Czech Republic, 2001. 148 p.
• M. Ceska, V. Janousek, and T. Vojnar. Generating and Using State Spaces of Object-Oriented Petri Nets. International Journal of Computer Systems Science and Engineering, 16(3):183--193, 2001.
• M. Ceska, V. Janousek, and T. Vojnar. Analysis and Verification Queries over Object-Oriented Petri Nets. In Proc. of 8th International Workshop on Computer Aided Systems Theory---EUROCAST'01, volume 2178 of LNCS, pages 365--384, 2001. Springer-Verlag.
• R. Koci and T. Vojnar. A PNtalk-based Model of a Cooperative Editor. In Proc. of MOSIS'01, Hradec nad Moravici, Czech Republic, pages 165--172, 2001. MARQ Ostrava.
• B. Krena and T. Vojnar. Type Analysis in Object-Oriented Petri Nets. In Proc. of ISM'01, Hradec nad Moravici, Czech Republic, pages 173--180, 2001. MARQ Ostrava.

2000 

• M. Ceska, V. Janousek, and T. Vojnar. Towards Verifying Distributed Systems Using Object-Oriented Petri Nets. In Proc. of 7th International Workshop on Computer Aided Systems Theory---EUROCAST'99, volume 1798 of LNCS, pages 90--104, 2000. Springer-Verlag.
• M. Ceska, V. Janousek, and T. Vojnar. Generating and Exploiting State Spaces of Object-Oriented Petri Nets. In Proc. of Workshop on Software Engineering and Petri Nets---SEPN'00, Aarhus, Denmark, DAIMI PB-548, pages 35--54, 2000. Department of Computer Science, University of Aarhus.
• M. Ceska, V. Janousek, and T. Vojnar. PNtalk Modelling Experience. In Proc. of 26th ASU Conference, La Valetta, Malta, pages 65--73, 2000. ASU and University of Malta, Faculty of Science, Department of Statistics and Operations Research.

1998 

• M. Ceska, V. Janousek, and T. Vojnar. Object-Oriented Petri Nets, Their Simulation, and Analysis. In Proc. of IEEE System, Man, and Cybernetics Conference---SMC'98, San Diego, California, USA, IEEE Catalog Number 98CH36218, pages 256--261, 1998. Omnipress.
• M. Ceska, V. Janousek, and T. Vojnar. PNtalk--An Experimental System Based on Object-Oriented Petri Nets. In Tool Demonstrations within 19th International Conference on Application and Theory of Petri Nets---ICATPN'98, Lisbon, Portugal, 1998.
• V. Janousek and T. Vojnar. State Spaces of Object-Oriented Petri Nets. In Proc. of MFCS'98 Workshop on Concurrency, Brno, Czech Republic, Technical Report FIMU-RS-98-06, pages 87--96, 1998. Faculty of Informatics, Masaryk University, Brno, Czech Republic.

1997 

• M. Ceska, V. Janousek, and T. Vojnar. PNtalk--A Computerized Tool for Object Oriented Petri Nets Modelling. In Proc. of 6th International Workshop on Computer Aided Systems Theory---EUROCAST'97, volume 1333 of LNCS, pages 591--610, 1997. Springer-Verlag.
• M. Ceska, V. Janousek, and T. Vojnar. PNtalk--A Language and System Based on Object Oriented Petri Nets. In Tool Demonstrations within 18th International Conference on Application and Theory of Petri Nets---ICATPN'97, Toulouse, France, 1997.
• T. Vojnar. Various Kinds of Petri Nets in Simulation and Modelling. In Proc. of MOSIS'97, Hradec nad Moravici, Czech Republic, pages 227--232, 1997. MARQ Ostrava.