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 analysis and verification (static analysis, abstract interpretation, model checking), 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]

Older photos of the group: 2012, 2013.

Research interests

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.

Awards

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

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.

Cooperation

Our group cooperates with many other teams within the Czech republic as well as abroad.  For example, we currently cooperate quite actively with:
  • Members of the consortium of the H2020 ECSEL project Arrowhead Tools,
  • Members of the consortium of the H2020 ECSEL project Aquas.

Your IPv4 address: 3.227.233.6
Switch to https