Automated Analysis and Verification Research Group - VeriFIT
VeriFIT is a group including researchers and students from FIT BUT interested in research on methods of automated analysis and verification of systems. The interests of the group include formal verification (model checking, static analysis), dynamic analysis (i.e., analysis at run-time), intelligent testing as well as methods of self-healing of systems. The group is involved in basic research in the described areas as well as in development and evaluation of prototype verification tools.
- Automated formal verification of infinite-state systems (such as systems with dynamic linked data structures like various kinds of lists or trees -- including their variants used, e.g., in the Linux kernel, unbounded integer variables, arrays, parameters, recursion, unbounded communication channels, etc.), using especially automata and various logics.
- Research on efficient techniques of handling automata and logics (e.g., simulation reduction of non-deterministic automata, efficient inclusion checking on non-deterministic automata---cf. www.languageinclusion.org---etc.).
- Automated verification and bug finding in concurrent software using a broad spectrum of approaches (static and dynamic analysis, intelligent testing, model checking), as well as automated self-healing of software.
- 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,
T. Vojnar) received the EATCS Best Theory Paper award of ETAPS'10.
- The paper Composed Bisimulation for Tree Automata (P.A. Abdulla,
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
Verification of C programs manipulating dynamic linked data structures based on pointers:
Verification of (concurrent) Java and C/C++ programs:
- Forester -- a tool for analysing programs with dynamic linked data structures using tree automata.
- Predator -- a tool for checking manipulation of dynamic data structures using separation logic.
- 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.
Tools for handling non-deterministic word and tree automata:
- 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.
Verification of hardware:
-- 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 real-time systems:
- 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).
- 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
- LIAFA, Université Paris 7 -- Denis Diderot/CNRS
- VERIMAG, Université Joseph Fourier/INPG/CNRS, Grenoble -- the program verification group
- IIS, Academia Sinica, Taiwan
- Software Systems Lab, University of Passau, Germany
- LFCS, University of Edinburgh
- LTA, DISCo, University Milano Bicocca
- IBM Haifa Research Laboratories
- Faculty of informatics, Masaryk University in Brno -- including, e.g., a common doctoral project Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems of the Czech Grant Agency and the MEMICS workshop organized within this project.