Research group AVELAB

Areas of Interest

The areas of interest include the following – with new exciting subjects in related areas always welcome:

• Static as well as dynamic analysis and verification of software or, more generally, computer-based systems: from low-level system software, such as the Linux kernel, its components and surrounding systems, through microservices to models and high-level specifications of safety-critical control systems, e.g., from the aerospace domain.
• Formal verification as well as testing. Symbolic execution, abstract interpretation, model checking, program slicing, fuzz testing and similar techniques.
• Analysis and verification of both functional properties (memory safety, concurrency safety, etc.) and non-functional ones (e.g., performance).
• Generation and validation of verification witnesses for both erroneous and correct code.
• Equivalence checking, e.g., preservation of the semantics after optimizations, refactoring, and security patches.

• SMT solving and decision procedures for various logics applied mostly as back-end techniques of analysis and verification methods, e.g., separation logic and theory of bitvectors.
• Answer set programming, logical programming, production systems (such as CLIPS/LEAPS).

• High-level languages for embedded control systems: from JavaScript to rule-based production systems (expert systems) such as CLIPS/LEAPS – often requiring advanced analysis and verification for efficiency and reliability.
• Static analysis methods for use in compilers of both high-level and low-level languages.
• Development methods and tools for embedded systems, esp. robotics.
• Front-ends, visualisation, and integration of tools (not only) for analysis and verification.

• Automata theory, algorithms, and tools with applications not only in analysis and verification.
• Algorithms and tools for efficient use of binary decision diagrams (BDDs).

Developed Tools

AVELAB researchers are involved in the development of multiple analysis and verification tools, some of them with successes in various competitions, others already in use in production (with new people to help in further development always wanted).

• Astral — decision procedure for separation logic (collaboration with VeriFIT).
• Broom — static analysis of safe memory usage in low-level code (collaboration with VeriFIT and TU Wien).
• DiffKemp — equivalence checking of low-level code (collaboration with Red Hat and VeriFIT).
• Fizzer — gray-box fuzzer for C programs.
• LTL3BA — translation of linear temporal logic (LTL) formulas to generalized transition-based Büchi automata.
• LTL3TELA — translation of linear temporal logic (LTL) formulas to Emerson-Lei automata.
• Perun — tool suite for performance analysis of programs (collaboration with Red Hat and VeriFIT).
• Q3B — SMT solver for quantified bit-vector formulas.
• RacerF — detection of race-conditions in low-level code (collaboration with VeriFIT).
• Seminator — semi-determinization and complementation of nondeterministic omega-automata.
• Symbiotic — framework for analysis and verification of C programs.
• Witch — a validator of verification witnesses of C programs.

Collaboration

We cooperate tightly with industrial partners and with researchers from other academic institutions.

• Honeywell
• NextSilicon
• Oracle Labs
• Red Hat

• CEA List Paris
• Fondazione Bruno Kessler
• LRE, Epita
• LSV, ENS Paris Saclay
• SoSy-Lab, LMU Munich
• TU Wien
• VeriFIT, FIT BUT

Members

• Jiří Barnat
• Ivana Černá
• Martin Jonáš
• Petr Ročkai
• Jan Strejček
• Marek Trtík
• Tomáš Vojnar