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. Whereas simulation-based timing-analysis techniques, most notably static timing analysis (STA) and statistical STA (SSTA), are the undisputed state-of-the-art for validating the timing correctness of modern very-large-scale digital integrated circuits, there remains room for complementary approaches. First, traditional STA/SSTA approaches can report timing violations but lack the ability to identify their most important causes. From a design-optimization viewpoint, however, there is a growing need for analyses that not only flag violations but also explain them and expose actionable sensitivities that guide low-effort design fixes. NVIDIA's recent INSTA framework [2] is, to the best of our knowledge, the first approach that also targets this issue. In essence, it replaces the min and max functions traditionally used for describing gate timing behavior by soft-min and soft-max, and leverages gradient-descent methods from modern machine learning to optimize critical delay values.

Second, to explore the detailed timing behavior of critical parts of a circuit, including asynchronous ones [3], dynamic digital timing analysis (DDTA) provides a much faster alternative to analog simulation (e.g., using SPICE). State-of-the-art DDTA techniques, which are based on pure or inertial delay models, offer modest timing prediction accuracy, however. Recent advances in discrete-value continuous-time history-aware gate delay models improved this situation. The most advanced instances are our novel hybrid delay models for multi-input gates [1], which provide analytic closed-form expressions for gate delays that cover both multi-input switching (delay variations due to closely timed transitions at different inputs) and drafting effects (delay variations due to an input transition close to the previous output transition). Besides considerably improving the accuracy of simulation-based DDTA [4], these expressions are also amenable to symbolic manipulation and sensitivity analysis.

As a consequence, our delay formulas unlock novel approaches for symbolic timing analysis. Our prototype tool [5] produces transition-time formulas (computed by a computer-algebra tool) in terms of symbolic input transition times and symbolic gate parameters, rather than explicit transition times as in simulation-based approaches. For each gate in the circuit, it automatically determines the relevant transition case and applies the corresponding delay formula to compute the symbolic output transition times. We combine this with a specifically tailored symbolic execution approach, which prunes paths in a given circuit that have no chance to contribute to some desired goal (like maximizing some critical delay), thus reducing the number of candidate delay formulas that need to be considered. This results in a reasonably generic symbolic timing analysis framework.

At the core of our symbolic execution approach is the avoidance of explicitly constructing complex timing formulas with min/max operators. Instead, we build a structured, model-agnostic representation of the state space, independent of the particular gate delay formula, from simple constraint delays to highly analytic expressions, and prune it by continuously restricting the parameter space using purely symbolic constraints. We establish sufficient conditions (e.g., dominance under the current constraints and monotonicity of the objective) that guarantee the soundness of pruning, and we show how symbolic contradictions yield lightweight certificates for discarded subtrees. This enables the efficient search for delay-formula parameters that optimize arbitrary objectives (e.g., minimizing/maximizing critical delays).

Beyond critical-delay optimization, the framework accommodates objectives such as minimizing worst-case arrival times or maximizing path slack. Another potential application lies in path validation for automated verification pipelines. Given a candidate timing permutation, the framework can symbolically compute all delays and check whether the presumed ordering with the symbolic execution is consistent with the resulting arrival times, offering a more scalable alternative to exhaustive SPICE-based validation. The talk will present the framework in full and demonstrate how efficient state-space pruning unlocks powerful optimization techniques for symbolic timing analysis.

REFERENCES [1] A. Ferdowsi, M. F¨ugger, T. Nowak, U. Schmid, and M. Drmota, “Faithful dynamic timing analysis of digital circuits using continuous thresholded mode-switched ODEs,” Nonlinear Analysis: Hybrid Sys- tems, vol. 56, p. 101572, 2025. doi: 10.1016/j.nahs.2024.101572 [2] Y.-C. Lu, Z. Guo, K. Kunal, R. Liang, and H. Ren, “INSTA: An Ultra-Fast, Differentiable, Statistical Static Timing Analysis Engine for Industrial Physical Design Applications“ [3] A. J. Winstanley, A. Garivier, and M. R. Greenstreet, “An event spacing experiment,” in Proc. 8th Int. Symp. Asynchronous Circuits and Systems (ASYNC), 2002, pp. 176–185. doi: 10.1109/ASYNC.2002.1000094 [4] A. Ferdowsi, U. Schmid, M. F¨ugger, J. Salzmann, and E. Thaqi, “Incorporating drafting and multi-input switching in digital dynamic timing analysis,” in preparation, 2025. [5] E. Thaqi, D. Eigner, A. Ferdowsi, U. Schmid, “Symbolic Timing Analysis of Digital Circuits Using Analytic Delay Functions”, submitted, 2025.

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.