2023

A symbolic algorithm for the case-split rule in solving word constraints with extensions (technical report), report, 2023
Authors: HAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A.

Modular Mix-and-Match Complementation of Büchi Automata (Technical Report), report, 2023
Authors: HAVLENA, V.; ŠMAHLÍKOVÁ, B.; LENGÁL, O.; LI, Y.; TURRINI, A.

2022

Complementing Büchi Automata with Ranker (Technical Report), report, 2022
Authors: HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.

Low-Level Bi-Abduction (Artifact), other unclassified results, 2022
Authors: ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F.

Low-Level Bi-Abduction (technical report), report, 2022
Authors: HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F.

Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation (Technical Report), report, 2022
Authors: HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.

2021

Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report), report, 2021
Authors: HAVLENA, V.; LENGÁL, O.

2020

Learning Probabilistic Automata in the Context of IEC 104, report, 2020
Authors: HAVLENA, V.; HOLÍK, L.; MATOUŠEK, P.

String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report), report, 2020
Authors: HOLÍK, L.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P.

2019

Automata Terms in a Lazy WSkS Decision Procedure (Technical Report), report, 2019
Authors: HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T.

PredatorHP Attacks Interval-Sized Regions, report, 2019
Authors: KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T.

Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report), report, 2019
Authors: HOLÍK, L.; HOLÍKOVÁ, L.; LENGÁL, O.; VOJNAR, T.; SAARIKIVI, O.; VEANES, M.

2018

Simulation Algorithms for Symbolic Automata (Technical Report), report, 2018
Authors: HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M.

2017

An Executable Sequential Specification for Spark Aggregation, report, 2017
Authors: LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B.

Lazy Automata Techniques for WS1S, report, 2017
Authors: FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T.

Register Automata with Linear Arithmetic, report, 2017
Authors: LENGÁL, O.; CHEN, Y.; TAN, T.; WU, Z.

2016

From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03, report, 2016
Authors: DUDKA, K.; HOLÍK, L.; PERINGER, P.; TRTÍK, M.; VOJNAR, T.

2014

Compositional Entailment Checking for a Fragment of Separation Logic, report, 2014
Authors: ENEA, C.; LENGÁL, O.; SIGHIREANU, M.; VOJNAR, T.

Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors, report, 2014
Authors: CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.

2013

Byte-Precise Verification of Low-Level List Manipulation, report, 2013
Authors: DUDKA, K.; PERINGER, P.; VOJNAR, T.

Fully Automated Shape Analysis Based on Forest Automata, report, 2013
Authors: HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.

The Tree Width of Separation Logic with Recursive Definitions, report, 2013
Authors: ROGALEWICZ, A.; ŠIMÁČEK, J.; IOSIF, R.

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata, report, 2013
Authors: HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P.

2012

Testing of Concurrent Programs Using Genetic Algorithms, report, 2012
Authors: DUDKA, V.; KŘENA, B.; LETKO, Z.; VOJNAR, T.

Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures, report, 2012
Authors: ZACHARIÁŠOVÁ, M.; LENGÁL, O.

2011

Advanced Ramsey-based Büchi Automata Inclusion Testing, report, 2011
Authors: ABDULLA, P.; CHEN, Y.; CLEMENTE, L.; HOLÍK, L.; HONG, C.; MAYR, R.; VOJNAR, T.

DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, report, 2011
Authors: DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T.

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, report, 2011
Authors: HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.

Forest Automata for Verification of Heap Manipulation, report, 2011
Authors: HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P.

HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, report, 2011
Authors: ZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M.

Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, report, 2011
Authors: DUDKA, K.; PERINGER, P.; VOJNAR, T.

2010

A Uniform Classification of Common Concurrency Errors, report, 2010
Authors: FIEDOR, J.; KŘENA, B.; LETKO, Z.; VOJNAR, T.

Fast Acceleration of Ultimately Periodic Relations, report, 2010
Authors: BOZGA, M.; IOSIF, R.; KONEČNÝ, F.

Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, report, 2010
Authors: HOLÍK, L.; VOJNAR, T.; CHEN, Y.; MAYR, R.; HONG, C.; ABDULLA, P.; CLEMENTE, L.

When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata), report, 2010
Authors: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R.

2009

A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing, report, 2009
Authors: LETKO, Z.; VOJNAR, T.; KŘENA, B.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S.

Automatic Verification of Integer Array Programs, report, 2009
Authors: IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M.

Mediating for Reduction (On Minimizing Alternating Büchi Automata), report, 2009
Authors: ABDULLA, P.; HOLÍK, L.; CHEN, Y.; VOJNAR, T.

Mediating for Reduction (On Minimizing Alternating Büchi Automata), report, 2009
Authors: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.

Optimizing an LTS-Simulation Algorithm, report, 2009
Authors: HOLÍK, L.; ŠIMÁČEK, J.

2008

A Logic of Singly Indexed Arrays, report, 2008
Authors: HABERMEHL, P.; IOSIF, R.; VOJNAR, T.

A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata, report, 2008
Authors: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L.

Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata, report, 2008
Authors: HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T.

Composed Bisimulation for Tree Automata, report, 2008
Authors: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L.

Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata, report, 2008
Authors: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L.

What else is decidable about integer arrays?, report, 2008
Authors: HABERMEHL, P.; IOSIF, R.; VOJNAR, T.

2007

SHADOWS - Deliverable D3.2.1: Research Report on Methodology for Self-Healing Concurrent Code Fixing, report, 2007
Authors: KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T.

SHADOWS - Deliverable D3.2.3: Report on Safety of Program Modifications, report, 2007
Authors: DUDKA, V.; KŘENA, B.; LETKO, Z.; VOJNAR, T.

2005

CRC64 Algorithm Analysis and Verification, report, 2005
Authors: HLÁVKA, P.; KRATOCHVÍLA, T.; ŘEHÁK, V.; ŠAFRÁNEK, D.; ŠIMEČEK, P.; VOJNAR, T.