Přístupnostní navigace
E-application
Search Search Close
prof. Ing.
Ph.D.
FIT, RG VERIFIT – Chairman of Workgroup
+420 54114 1202vojnar@fit.vut.cz
Send BUT message
2022
HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F. Low-Level Bi-Abduction (technical report). Ithaca: 2022. 43 p.
ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F. Low-Level Bi-Abduction (Artifact). Dagstuhl: 2022. p. 1-6.
2020
HOLÍK, L.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P. String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). New York: Springer International Publishing, 2020. p. 1-33.
2019
HOLÍK, L.; HOLÍKOVÁ, L.; LENGÁL, O.; VOJNAR, T.; SAARIKIVI, O.; VEANES, M. Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report). Ithaca: Cornell University Library, 2019. p. 1-19.
KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T. PredatorHP Attacks Interval-Sized Regions. Ithaca: 2019. p. 1-4.
HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). Ithaca: 2019. p. 1-25.
2018
HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca: 2018. p. 1-23.
2017
FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. arXiv:1701.06282: 2017. 17 p.
HRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. Brno: Faculty of Information Technology BUT, 2017. p. 1-23.
2016
DUDKA, K.; HOLÍK, L.; PERINGER, P.; TRTÍK, M.; VOJNAR, T. From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03. Brno: 2016. p. 1-28.
2014
ENEA, C.; LENGÁL, O.; SIGHIREANU, M.; VOJNAR, T. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Faculty of Information Technology BUT, 2014. p. 1-19.
CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. Brno: Faculty of Information Technology BUT, 2014. 18 p.
2013
HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013. p. 1-35.
DUDKA, V.; KŘENA, B.; LETKO, Z.; ŠIMKOVÁ, H.; VOJNAR, T. Testing Concurrent Programs Using Multi-objective Genetic Algorithms. FIT-TR-2013-05, Brno: 2013. 35 p.
HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013. p. 1-25.
DUDKA, K.; PERINGER, P.; VOJNAR, T. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013. 48 p.
2012
DUDKA, V.; KŘENA, B.; LETKO, Z.; VOJNAR, T. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno: 2012. 31 p.
2011
HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Faculty of Information Technology BUT, 2011. 22 p.
HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. 30 p.
DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Faculty of Information Technology BUT, 2011. 9 p.
DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. FIT-TR-2011-02, Brno: Faculty of Information Technology BUT, 2011. 23 p.
ABDULLA, P.; CHEN, Y.; CLEMENTE, L.; HOLÍK, L.; HONG, C.; MAYR, R.; VOJNAR, T. Advanced Ramsey-based Büchi Automata Inclusion Testing. FIT-TR-2011-03, Brno: Faculty of Information Technology BUT, 2011. 45 p.
2010
HOLÍK, L.; VOJNAR, T.; CHEN, Y.; MAYR, R.; HONG, C.; ABDULLA, P.; CLEMENTE, L. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010. 30 p.
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). FIT-TR-2010-01, Brno: Faculty of Information Technology BUT, 2010. 22 p.
FIEDOR, J.; KŘENA, B.; LETKO, Z.; VOJNAR, T. A Uniform Classification of Common Concurrency Errors. FIT-TR-2010-03, Brno: 2010. 24 p.
2009
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. 49 p.
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009. 29 p.
LETKO, Z.; VOJNAR, T.; KŘENA, B.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno: 2009. 15 p.
ABDULLA, P.; HOLÍK, L.; CHEN, Y.; VOJNAR, T. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009. 26 p.
2008
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. 19 p.
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno: 2008. 19 p.
HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008. 15 p.
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno: 2008. 18 p.
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno: 2008. 34 p.
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. 36 p.
2007
KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T. SHADOWS - Deliverable D3.2.1: Research Report on Methodology for Self-Healing Concurrent Code Fixing. Brno: European Comission EU, 2007. 13 p.
DUDKA, V.; KŘENA, B.; LETKO, Z.; VOJNAR, T. SHADOWS - Deliverable D3.2.3: Report on Safety of Program Modifications. Brno: European Comission EU, 2007. 21 p.
2005
HLÁVKA, P.; KRATOCHVÍLA, T.; ŘEHÁK, V.; ŠAFRÁNEK, D.; ŠIMEČEK, P.; VOJNAR, T. CRC64 Algorithm Analysis and Verification. Brno: CESNET National Research and Education Network, 2005. 7 p.
2004
BOUAJJANI, A.; VOJNAR, T. Integration of tools for the analysis of parameterized systems and dynamic networks, Finalized common validation framework. Paříž: 2004. 14 p.
2003
JANOUŠEK, V.; VOJNAR, T.: xx; PNtalk system (v. 96). xx. URL: http://www.daimi.au.dk/PetriNets/tools/db/pntalk.html. (produkt nebo technologie ve stavu vývoje, testování)
2002
BOUAJJANI, A.; VOJNAR, T. Automata with Parameterized Arrays and Parameterized Networks of Automata. Paris: The Information Society Technologies (IST) programme of the EU Fifth Framework Programme, 2002. 13 p.
BOUAJJANI, A.; HABERMEHL, P.; VOJNAR, T. Verification of Parameterized Concurrent Systems with Resource Sharing. Paris: The Information Society Technologies (IST) programme of the EU Fifth Framework Programme, 2002. 27 p.
*) Citace se generují jednou za 24 hodin.