ABSTRACT. MBSE is a prevalent methodology for designing complex systems and systems of systems. When proving the correctness and safety of such systems, it is important to ensure all parties agree on the semantics of the models: the engineers who design the model, the designers who create the language specification, and the tool vendors who develop simulators and verifiers for the language. Unfortunately, today's MBSE languages (such as SysML) do not have well-defined execution semantics, thus discrepancies between the aforementioned parties is frequent. As a result, each team of engineers has to use a customized verification toolchain, which is usually too costly to be viable in practice.

My research focuses on creating a framework that allows the specification of the semantics of modeling languages in a configurable and reusable fashion, which is expected to 1) decrease the effort needed to customize tools and toolchains; 2) provide a whole family of verification backends for each tool; and 3) help language designers ensure consistent execution semantics for their language.

ABSTRACT. Model checking allows us to verify properties of powerful temporal logics such as mu-calculus. Abstraction-refinement approaches such as Counterexample-guided Abstraction Refinement (CEGAR) or Three-valued Abstraction Refinement (TVAR) allow us to generate and refine increasingly precise Kripke structures used for model-checking. However, generating the transitions soundly and precisely from programming-language-style step descriptions is not easy. I will discuss how we can connect an abstraction-refinement framework for model-checking to dataflow analyses and specifically abstract interpretation that compute the Kripke structure transitions, leveraging the advantages of both.

ABSTRACT. We propose a method to synthesize a parameterized infinite-state systems that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as parameter variables that encode properties of the environment. Our synthesis method runs in a counterexample-guided loop consisting of four main steps: First, we use existing techniques to synthesize concrete systems for some small parameter instantiations. Second, we generalize the concrete systems into a parameterized program. Third, we create a proof candidate consisting of an invariant and a ranking function. Fourth, we check the proof candidate for consistency with the program. If the proof succeeds, the parameterized program is valid. Otherwise, we identify a parameter value for which the proof fails and add a new concrete instance to step one. To generalize programs and create proof candidates, we use a combination of anti-unification and syntax-guided synthesis to express syntactic differences between programs as functions of the parameters. We evaluate our approach on examples from the literature that have been extended with parameters as well as new problems.

ABSTRACT. Symbolic datatypes are central to abstract reasoning about dynamical systems. Successful examples include BDDs and SAT for finite-state systems, and polyhedra and SMT for discrete dynamical systems over certain infinite state spaces. Neural networks provide a natural symbolic datatype over continuous state spaces, with the added benefit of supporting key operations while being trainable. We advocate using neural networks for multiple purposes in reasoning about continuous state spaces, particularly for representing both deterministic dynamics—such as controllers—and correctness certificates. A correctness certificate is a succinct witness for a desired property of a dynamical system. For example, invariants and barrier functions certify safety, while Lyapunov functions and supermartingales certify progress. Stochastic barrier functions and supermartingales can further account for uncertainty (noise) in system dynamics. Established techniques from machine learning and formal reasoning about neural networks—such as SMT, abstract interpretation, and counterexample-guided refinement—enable the joint synthesis of controllers and correctness certificates. This allows for the synthesis of guaranteed-to-be-correct controllers, where both the controllers and their certificates are represented, learned, and verified as neural networks. This talk includes joint work with Krishnendu Chatterjee, Mathias Lechner, and Djordje Zikelic.

ABSTRACT. Back-references are a common regex extension as evidenced by them being supported by most major languages and regex matching tools. However, all of those tools resort to backtracking algorithms to match them, which have exponential worst case complexity. This makes matching regexes with back-references (rewbs) vulnerable to catastrophic slowdown, which can even constitute a security threat. We propose register set automata (RSAs), a model that generalises register automata to allow registers to store sets of symbols instead of individual symbols. A key property of RSAs is that one can determinise a large class of register automata (which are not determinisable in general) into deterministic RSAs. We use this property to match single-character rewbs (i.e., rewbs with capture groups of length 1) in a prototype implementation. The experimental evaluation of the prototype indeed confirms that it can significantly improve robustness of state-of-the-art regex matchers on single-character rewbs.

ABSTRACT. Formally analysing system requirements enables early detection of specification defects, which reduces costs later on. Our approach models individual formal requirements as timed automata and then analyses their intersection to detect undesirable properties. However, large sets of requirements can lead to long analysis times as a result of combinatorial complexity. To address this, we investigate a method to minimize the number of locations of a PEA without altering their semantics before the intersection operation. Specifically, we aim to merge automaton locations when equivalence can be proven, with the goal of constructing the smallest correct automaton equivalent to its formal requirement. This work in progress focuses on defining a minimization procedure, proving its correctness, and integrating it into our existing analysis tool.

ABSTRACT. Complementation is a central challenge in the theory of ω-automata, which are used to reason about infinite behaviors in systems such as reactive software and hardware. While complementation is well-understood for classical acceptance conditions like Büchi acceptance condition, the general Emerson-Lei acceptance—which is defined by arbitrary Boolean combinations of infinitely and finitely occurring events—poses new challenges. Recent advances introduced efficient, structure-aware algorithms for complementing these expressive automata, especially for the practically relevant subclass of elevator automata. By leveraging the structure of the acceptance condition, these methods achieve better complexity than classical approaches, making complementation more scalable for real-world verification tasks. This line of work advances both the theoretical foundations and practical capabilities of automata-based verification for infinite behaviors.

ABSTRACT. Active automata learning is a promising approach for the automated construction of system models in black-box settings. However, existing algorithms have issues scaling to large systems. The central challenge is to combine different observations into a structure that reflects the system behavior. To improve efficiency, most algorithms attempt to reduce redundancy wherever possible. In this talk, we take a look at a new learning algorithm that willingly accepts redundancy in a small part of its structure to further improve efficiency in the remaining part. Practical benchmarks indicate a reduction in overall complexity.

ABSTRACT. Quantum circuit simulation is a fundamental tool for analyzing quantum circuits and is therefore essential for further research in the emerging field of quantum computing. However, this task is very computationally demanding. Despite significant progress in recent years, the performance of state-of-the-art simulators still remains unsatisfactory for non-trivial circuits. In this work, we present an accurate simulation technique based on multi-terminal binary decision diagrams (MTBDDs) that utilizes symbolic execution to accelerate the simulation of repeated structures, such as loops, in quantum circuits. Experimental results show that the implemented simulator outperforms state-of-the-art simulators by several orders of magnitude on some standard circuits, such as Grover’s algorithm.

ABSTRACT. We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavy-weight approaches while being faster than them.

ABSTRACT. Witnesses are a standardized exchange format between software verification tools, enabling reuse of verification results. While witnesses can be validated - and many validators exist - validating correctness witnesses is often slower than performing verification without a witness. If the goal is solely to verify the program, the information from a witness can instead be used as hints to accelerate verification, without validating the witness. We refer to this approach as witness-guided verification. In this talk, we demonstrate how witness-guided verification for correctness witnesses can be integrated into the trace abstraction algorithm to accelerate verification.