Tomas Vojnar – Publications

• T. Dacik, A. Rogalewicz, T. Vojnar, and F. Zuleger. Deciding Boolean Separation Logic via Small Models. In Proc. of 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'24, Luxembourg, volume 14570 of LNCS, pages 188–206, 2024. Springer-Verlag. The Astral decision procedure is available here. The associated technical report is here.
• V. Malik, P. Schrammel, and T. Vojnar. Template-Based Verification of Array-Manipulating Programs. Taming the Infinities of Concurrency – Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday, volume 14660 of LNCS, pages 206–224, 2024. Springer-Verlag. The paper is also available here.

• L. Holik, J. Sic, L. Turonova, and T. Vojnar. Fast Matching of Regular Patterns with Synchronizing Counting. In Proc. of 26th International Conference on Foundations of Software Science and Computation Structures – FoSSaCS'23, Paris, France, volume 13992 of LNCS, pages 392–412, 2008. Springer-Verlag.
• V. Malik, F. Necas, P. Schrammel, and T. Vojnar. 2LS: Arrays and Loop Unwinding (Competition Contribution). In Proc. of 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'23 as a competition contribution within the 12th International Competition on Software Verification – SV-COMP'23, Paris, France, volume 13994 of LNCS, pages 529–534, 2023. Springer-Verlag. The 2LS tool is available here. Collaboration with DiffBlue.
• D. Kozak, V. Jovanovic, C. Stancu, T. Vojnar, and C. Wimmer. Comparing Rapid Type Analysis with Points-To Analysis in GraalVM Native Image. In Proc. of the 20th International Conference on Managed Programming Languages and Runtimes – MPLR'23, Cascais, Portugal, pages 129–142, 2023. ACM. Collaboration with Oracle Labs.

• M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. SagTree: Towards efficient mutation in evolutionary circuit approximation. Swarm and Evolutionary Computation, 69(100986), 2022. Elsevier.
• L. Charvat, A. Smrcka, and T. Vojnar. Utilizing Parametric Systems for Detection of Pipeline Hazards. International Journal on Software Tools for Technology Transfer (STTT), 24(1):1–28, 2022. Springer-Verlag. A preliminary version is available here.
• L. Turonova, L. Holik, I. Homoliak, O. Lengal, M. Veanes, and T. Vojnar. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In Proc. of 31st USENIX Security Symposium, Boston, USA, pages 4165–4182, 2022. USENIX. The GadgetCA tool for ReDoS generation is available here. Collaboration with Microsoft Research Redmond.
• L. Holik, P. Peringer, A. Rogalewicz, V. Sokova, T. Vojnar, and F. Zuleger. Low-Level Bi-Abduction. In Proc. of 36th European Conference on Object-Oriented Programming – ECOOP'22, Berlin, Germany, volume 222 of LIPIcs, pages 19:1–19:30, 2022. Schloss Dagstuhl – Leibniz-Zentrum fur Informatik. The Broom tool is available here.
• O. Vasicek, J. Fiedor, T. Kratochvila, B. Krena, A. Smrcka, and T. Vojnar. Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC. In Proc. of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering – ESEC/FSE'22, Singapore, pages 408–1418, 2022. ACM. Available in pdf HERE as well. The Unite tool is available here. Collaboration with Honeywell.
• T. Fiedor, J. Pavela, A. Rogalewicz, and T. Vojnar. Perun: Performance Version System. In Proc. of the 38th IEEE International Conference on Software Maintenance and Evolution – ICSME'22, Limassol, Cyprus, pages 499–503, 2022. IEEE. The Perun tool is available here.
• M. Ceska, J. Matyas, V. Mrazek, and T. Vojnar. Designing Approximate Arithmetic Circuits with Combined Error Constraints. In Proc. of the 25th Euromicro Conference on Digital System Design – DSD'22, Maspalomas, Spain, pages 785–792, 2022. Euromicro.
• V. Malik, P. Silling, and T. Vojnar. Applying Custom Patterns in Semantic Equality Analysis. In Proc. of the 10th International Conference on Networked Systems – NETYS'22, volume 13464 of LNCS, pages 265–282, 2022. Springer-Verlag. The DiffKemp tool is available here. The best student paper award of NETYS'22. Collaboration with Red Hat.
• J. Fiedor, B. Krena, A. Smrcka, O. Vasicek, and T. Vojnar. Integrating OSLC Services into Eclipse. In Proc. of the 18th International Conference on Computer Aided Systems Theory – EUROCAST'21, Las Palmas, Spain, volume 13789 of LNCS, pages 240–249, 2022. Springer-Verlag. The Unite tool is available here. Collaboration with Honeywell.
• R. Andriushchenko, M. Ceska, V. Marcin, and T. Vojnar. GPU-Accelerated Synthesis of Probabilistic Programs. In Proc. of the 18th International Conference on Computer Aided Systems Theory – EUROCAST'21, Las Palmas, Spain, volume 13789 of LNCS, pages 258–266, 2022. Springer-Verlag.
• D. Harmim, V. Marcin, L. Svobodova, and T. Vojnar. Static Deadlock Detection in Low-Level C Code. In Proc. of the 18th International Conference on Computer Aided Systems Theory – EUROCAST'21, Las Palmas, Spain, volume 13789 of LNCS, pages 267–276, 2022. Springer-Verlag. The low-level deadlock detector L2D2 implemented as Meta Infer plugin is available here.

• 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, 2021. IEEE. A preliminary version is available here. The DiffKemp tool is available here. Collaboration with Red Hat.
• 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. 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. Collaboration with Microsoft Research Redmond.
• 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. Collaboration with DiffBlue.
• 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.

• 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. Collaboration with Microsoft Research Redmond.
• 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. Collaboration with DiffBlue.
• 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.

• 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. Collaboration with DiffBlue.
• 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. Collaboration with Microsoft Research Redmond.
• 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. Collaboration with Honeywell.
• 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. Collaboration with DiffBlue.
• 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.

• 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.

• 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.

• 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.

• 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 Buchi 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.

• 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.

• 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.

• 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 Buchi 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.

• 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 Buchi 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.

• P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar. Mediating for Reduction (On Minimizing Alternating Buchi 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.

• 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.

• 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.

• 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.

• 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, Saarbrucken, 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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.