Efficient Technology for Dealing with Logics and Automata (Not Only) for Formal Analysis and Verification -- co-supervised by dr. O. Lengal

This dissertation topic is available for Czech studies only.

Different types of logics and automata are among the most fundamental objects studied and applied in computer science for decades. Nevertheless, there are many unsatisfactorily solved problems in this area, and new, exciting problems related to ever new applications of logics and automata are constantly emerging (e.g., in the formal verification of finite and infinite state systems with various advanced control or data structures, in decision procedures, in program or hardware synthesis, in quantum program verification, or even in methods for efficient search in various types of data or network traffic).

The subject of the dissertation will primarily be the development of the state of the art in efficient work with various logics (e.g. over pointer structures, strings, various arithmetic, temporal logics, etc.). To this end, approaches based on different types of decision diagrams, automata, but also e.g. approaches based on the existence of a model of bounded size or on efficient reductions between different types of logical theories will be investigated. In connection with this, methods for efficient work with decision diagrams and different types of automata (automata over words, trees, infinite words, automata with counters, etc.) will be developed. The work will include theoretical research as well as prototype implementation of the proposed techniques and their experimental evaluation.

The work will be solved in collaboration with the VeriFIT team working on the development of techniques for working with logics and automata and their applications at FIT BUT. In particular, Dr. O. Lengal will act as a specialist trainer. After the completion of Dr. Lengal's habilitation, it is expected that he will move to the role of principal supervisor, while T. Vojnar may continue to remain in the role of specialist supervisor. There is also the possibility of close cooperation with various foreign partners of VeriFIT: Academia Sinica, Taiwan (Prof. Y.- F. Chen); TU Vienna, Austria (Assoc. F. Zuleger); LSV, ENS Paris-Saclay (Assoc. M. Sighireanu); IRIF, Paris, France (Assoc. A. Bouajjani, Assoc. P. Habermehl, Assoc. C. Enea), Verimag, Grenoble, France (Assoc. R. Iosif); Uppsala University, Sweden (prof. P.A. Abdulla, prof. B. Jonsson); or School of Informatics, University of Edinburgh, UK (prof. R. Mayr).

Within the framework of the topic, the student can also actively participate in various grant projects, such as. Representation of Boolean Functions using Adaptive Data Structure", GA23-06506S "AIDE: Advanced Analysis and Verification for Advanced Software", the newly accepted GA project 25-18318S "QUAK: Quantum Program Analysis using Automata Toolkit", or the Horizon Europe project SEP-210979090 "VASSAL: Verification and Analysis for Safety and Security of Applications in Life".