Logic and Automata

There is a tight connection between certain logics and automata which can be used, for example, to devise decision procedures for problems in software verification.

Expressive Power

The study of the expressive power of various formalisms is a central topic in mathematics. In our group we investigate the expressive power of certain logics using tools from logic, automata theory, and algebra. The focus lies on monadic second-order logic and its fragments over infinite trees and various graph classes.

Automata Engineering

Automata on infinite words are cornerstones of many algorithms for verification, analysis, or synthesis of reactive systems. We study translation of linear temporal logic (LTL) to classes of automata with various structural properties (e.g., deterministic, nondeterministic) and acceptance conditions (e.g., Büchi, Emerson-Lei, parity). Further, we develop techniques for efficient automata reductions and transformations, and also algorithms processing automata.

SMT Solving

Satisfiability modulo theory (SMT) solving studies algorithms deciding whether a given formula is satisfiable in a given theory. These algorithms are implemented in SMT solvers, which have numerous applications. We primarily focus on SMT solving of bitvector theory, which is a crucial component of many program analysis tools based on bounded model checking or symbolic execution.

What We Do

Study Formalisms

We study expressive power of various logics and automata classes.
We analyze decidability and complexity of relevant problems.

Algorithms & Experiments

We develop algorithms for creation, reduction, transformation, and application of automata.
We propose algorithms for satisfiability and SMT solving.
We make intensive experiments to assess the efficiency of our algorithms compared to other existing approaches.