Static analysis, dynamic analysis and testing of computer systems, software quality assurance, and related subjects from the areas of automata theory and logics, including:

• Static analysis and verification with formal roots in the area of infinite-state systems (programs with pointers and dynamic linked data structures, concurrent programs with unbounded concurrency, programs with unbounded integer variables, arrays, parameters, recursion, unbounded communication channels, etc.), building on applications of theory of automata, logics, and graphs.
• Testing and dynamic analysis of (esp. concurrent) software using a broad range of techniques (such as noise injection, extrapolation, data mining, machine learning), including possible self-healing or providing information for software quality assurance.
• Formal verification in the area of hardware design based on high-level hardware description languages.
• Research on efficient techniques of handling automata (e.g., simulation reduction of non-deterministic automata or efficient inclusion checking on non-deterministic automata), decision procedures for various logics, etc.

• The tools Predator (P. Peringer, V. Sokova, T. Vojnar) and 2LS (V. Malík, T. Vojnar; the tool is being primarily developed by DiffBlue) took part in the International Software Verification Competition SV-COMP'20 where they won one gold and one bronze medal. Moreover, V. Sokova, M. Hruska, and T. Vojnar participated on a combination of Predator with the Symbiotic analyser that is being primarily developed at FI MU and that won one gold and two silver medals.
• The paper Chain-Free String Constraints (P.A. Abdulla, M.F. Atig, B.P. Diep, L. Holík, P. Janků) received the Best Paper award of ATVA 2019.
• The paper Automata Terms in a Lazy WSkS Decision Procedure (V. Havlena, L. Holik, O. Lengal, T. Vojnar) received the Best Paper award of CADE-27, 2019.
• The tools Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) and 2LS (V. Malík, T. Vojnar; the tool is being primarily developed by DiffBlue) took part in the International Software Verification Competition SV-COMP'19 where they won one silver medal, and Predator won the MemSafety-Heap and MemSafety-LinkedLists sub-categories.
• The paper about the ANaConDA analyzer won the best tool demo award at ISSTA'18.
• The approach proposed in collaboration with the ehw@FIT group and first presented in the paper Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished (M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar) won a bronze medal in the 2018 Human-Competitive Awards: "Humies" competition.
• V. Malík and J. Matyáš won the JCMM Brno PhD talent scholarship starting from the 2017 year.
• J. Matyáš won the IT SPY competition for the best diploma thesis of the year with his thesis "Employing Approximate Equivalence for Design of Approximate Circuits" led by M. Češka jr and solved in collaboration between the VeriFIT and ehw@fit groups.
• The Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) and Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) tools took part in the International Software Verification Competition SV-COMP'18 where they won one silver medal, and Predator won the ReachSafety-Heap and MemSafety-Heap categories. Moreover, some members of the group (V. Malík, Š. Martiček, T. Vojnar) got involved into the competition within the team of the 2LS analyser that is being primarily developed by the DiffBlue company.
• The Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) and Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) tools took part in the International Software Verification Competition SV-COMP'17 where they won one gold medal.
• Ondřej Lengál won the 2015 Antonín Svoboda Award for the Best Dissertation Thesis awarded by the Czech Society for Cybernetics and Computer Science.
• The Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) and Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) tools took part in the International Software Verification Competition SV-COMP'16 where they won one gold medal.
• The Predator (P. Müller, P. Peringer, T. Vojnar) and Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) tools took part in the International Software Verification Competition SV-COMP'15 where they won one gold and one silver medal.
• The SPEN (C. Enea, O. Lengál, M. Sighireanu a T. Vojnar) and SLIDE (R. Iosif, A. Rogalewicz a T. Vojnar) tools won one gold and three silver medals at the 1st International Competition of Separation Logic Decision Procedures SL-COMP'14.
• The Predator tool has been awarded the prestigious Kurt Gödel medal at the FLoC Olympic Games 2014 for its successes in three consecutive years of the international competition in software verification SV-COMP.
• The Predator (K. Dudka, P. Peringer, T. Vojnar) and CPAlien (P. Müller, T. Vojnar) tools took part in the International Software Verification Competition SV-COMP'14 where they won one silver and one bronze medal.
• The paper The Tree Width of Separation Logic with Recursive Definitions (R. Iosif, A. Rogalewicz, J. Simacek) received the Best Paper award of CADE-24, 2013.
• The paper An Integrated Specification and Verification Technique for Highly Concurrent Data Structures (P.A. Abdulla, F. Haziza, L. Holík, B. Jonsson, A. Rezine) received the EASST Best Software Science Paper award of ETAPS'13.
• The Predator tool (K. Dudka, P. Müller, P. Peringer, T. Vojnar) won three categories of the SV-COMP'13 competition.
• The paper ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level (J. Fiedor, T. Vojnar) received the Best Tool Paper award of RV'12.
• The Predator tool (K. Dudka, P. Müller, P. Peringer, T. Vojnar) won one of the categories of the SV-COMP'12 competition.
• The paper When Simulation Meets Antichains. On Checking Language Inclusion of NFAs. (P.A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr, T. Vojnar) received the EATCS Best Theory Paper award of ETAPS'10.
• The paper Composed Bisimulation for Tree Automata (P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, T. Vojnar) received the Best Paper award of CIAA'08.

Most of the results, published in our papers, include an experimental evaluation on a prototype implementation. Here are some of the tools that we have developed (the others may be provided if you sent us a request by email).

Plugins for analysing various program properties within various static analysers (primarily for the C/C++ languages).

• The plugins are developed for selected properties such as absence of deadlocks, atomicity of call sequences, or computational complexity and implemented on top of analysers such as Facebook Infer or Frama-C.

Verification of C programs manipulating dynamic linked data structures based on pointers:

• Predator -- a tool for analysing programs with various kinds of dynamic linked lists using symbolic memory graphs.
• 2LS -- the analyser is being primarily developed by DiffBlue, but members of the VeriFIT group participates on adding various features into the tool (e.g., analysis of programs with pointers or analysis of non-termination).
• Forester -- a tool for analysing programs with dynamic linked data structures using tree automata.
• CPAlien  -- a tool for analysing programs with dynamic linked data structures using symbolic memory graphs in the context of configurable program analysis.
• Code-listener -- an infrastructure for building static analyzers on top of GCC compiler.
• ARTMC -- a tree-automata based tool for verifying programs operating on complex dynamic data structures linked through pointers.

Performance analysis:

• Perun -- a tool for dynamic performance analysis and automated detection of performance regressions between different version of programs stored in repositories.
• Ranger -- a tool for resource-bounds analysis of heap-manipulating programs based on the Forester and Loopus tools.

Decision procedure:

• Sloth and Trau -- decision procedures for formulae over strings.
• Gaston -- a decition procedure for the WS1S logic based on-the-fly state-space search (an extension of the dWiNA prototype).
• dWiNA -- a decision procedure for the WS1S logic based on non-deterministic automata as an alternative to the very well-known MONA tool, which is based on using deterministic automata.
• SPEN -- a decision procedure for a fragment of separation logic with inductive predicates over lists using a combination of graph homomorphism checking, SAT solving, and checking membership in languages of tree automata.
• SLIDE -- a decision procedure for a fragment of separation logic with complex inductive predicates based on a reduction to checking inclusion of tree automata languages.

Verification of (concurrent) Java and C/C++ programs:

• SearchBestie -- a generic infrastructure for applications of search techniques in the field of program testing.
• ANaConDA -- an environment for dynamic analysis of concurrent C/C++ programs on the binary level
• DA-BMC -- a tool suite for dynamic analysis of concurrent Java programs, recording suspicious executions, and their subsequent reproduction and further examination in the JPF model checker (formerly RecRev).
• Java Race Detector and Healer -- a tool for a run-time detection and automatic healing of race conditions in concurrent Java programs.
• MUSE -- a tool for model checking using symbolic execution.

A collection of benchmarks that we use in our experiments with testing and dynamic analysis of concurrent software is available HERE.

Tools for handling non-deterministic word and tree automata:

• libVATA -- a library for efficient handling of explicitly as well as semi-symbolically encoded non-deterministic tree automata (an older version of the semi-symbolic part of the library used to be available as libSFTA).
• SA -- a tool for computing simulations over labelled transition systems (LTS) and tree automata (TA).

Verification of hardware:

• Hades -- a tool for detecting various kinds of hazards in single pipelined microprocessors using a combination of various formal methods (dataflow analysis, SAT solving, parameterized model checking).
• CDCreloaded -- a tool for formal verification of asynchronous circuits wit multiple clock domains.
• VHDL2CA -- a tool for compiling parametric VHDL components into counter automata that may be subsequently used for a formal verification of the components for all possible values of the parameters (using existing tools for formal verification over counter automata).

Verification of real-time systems:

• Zetav & Verif -- tools for verification of systems specified in RT-Logic language or the Modechart formalism.

Our group cooperates with many other teams within the Czech republic as well as abroad.  For example, we currently cooperate quite actively with:

• Department of Information Technology, Uppsala University, Sweden,
• Microsoft Research Redmond, USA,
• IIS, Academia Sinica, Taiwan,
• Department of Computer Science, Oxford University, UK,
• Software Modeling and Verification Group, RWTH Aachen, Germany,
• Institute of Theoretical Computer Science, TU Braunschweig, Germany,
• VERIMAG, University Grenoble Alpes/CNRS, Grenoble, France,
• FORSYTE, Faculty of Informatics, TU Vienna, Vienna, Austria,
• Chair for Foundations of Software Reliability and Theoretical Computer Science, TU Munich, Germany,
• Automatic Reasoning, Faculty of Informatics, TU Keiserslautern, Germany,
• IRIF, University Paris Diderot/CNRS, Paris, France, UK.

• D3S, MFF UK, Prague, Czechia,
• Fakulta informatiky, Masaryk University, Brno, Czechia.

• Red Hat Lab, Red Hat Czech at FIT BUT, Brno, Czechia,
• Honeywell Aerospace and International, Brno, Czechia,
• DiffBlue, Oxford, UK.

• Members of the consortium of the H2020 ECSEL project Arrowhead Tools,
• Members of the consortium of the H2020 ECSEL project Aquas.