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.

[img]

Research interests

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

Awards

Seminar

Tool support

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:

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

Cooperation

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

Your IPv4 address: 23.22.252.150
Switch to IPv6 connection

DNSSEC [dnssec]