The Learning in Verification group (LiVe Lab) focuses on the interactions of machine learning and verification. Our research includes Explainable AI, Verification of Neural Networks, Stochastic Games and Control, Probabilistic Model Checking, Temporal Logics (mainly LTL, PCTL), and Automata Theory. Our research is applicable in the Robotics, Biomedical, and Automotive domains. The team is distributed between the Masaryk University Brno, Czech Republic, and the Technical University of Munich, Germany.
We develop runtime monitors for neural networks to improve their reliability.
We abstract neural networks to improve verification speed.
We apply machine learning to the LTL synthesis problem.
We design algorithms for translating LTL to different types of automata.
We develop methods for explaining controllers with decision trees.
We develop methods for explaining controllers via automata.
We develop value iteration algorithms for stochastic games.
We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.
We provide a highly user-friendly tool for Synthesis of Cyber-security models based on the attack-tree concept. It also features interfaces to a variety of other tools and model-checkers, as well as built-in analysis for uncertain values. Additionally, the CLI can be used to learn attack-trees from logfiles or other traces.
This tool implements the semi-quantitative analysis of Chemical Reaction Networks.
In this project we develop learning-based exploration heuristics for LTL Synthesis that exploit the semantic labelling of the underlying Automaton/Game.
Owl is designed to help researches in formal methods to work with ω-words, ω-automata and LTL.
We create a tool (Monitizer) that optimizes monitors on a NN for a specific task.
Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.
Automata Tutor is an online teaching tool that aids instructors and students in large courses on automata and formal languages with many different exercise types.