Workshop Program
Friday, April 10, 2026 (Room: TBA)
Saturday, April 11, 2026 (Room: TBA)
Abstract
Autonomous underwater vehicles need to navigate and execute certain tasks in submarine environments, which are characterized by severe sensor noise, limited communication, and strong environmental uncertainty. In a recently completed European Training Network "Reliable AI for Marine Robotics (REMARO)", we examined opportunities to employ deep-learning-based methods for perception, control, and decision making in this context. While neural networks come with impressive empirical performance, their deployment in safety-critical settings like this needs careful development. In this talk, we report on an approach to combine heuristic techniques for the robust synthesis of neural networks with formal analysis methods to increase the reliability of these systems.
Abstract
Software verification and software testing are valuable means of ensuring software quality. Many approaches in both fields employ software model checking. Although software model checking is a powerful technique, it can be time-consuming, which hinders its practical applicability. To address this issue, we present a parallelization of the model-checking technique trace abstraction. The underlying idea of our approach is to parallelize the abstraction-refinement process. More concretely, we analyze different potentially spurious counterexamples in parallel. We apply our approach to both software verification and test-case generation, and show that our technique not only improves response times for computationally expensive tasks, but also incurs only a small overhead for smaller tasks. Furthermore, we demonstrate how our multi-threaded framework can be extended to portfolio-style approaches by combining it with symbolic execution.
Abstract
Autonomous agents trained in simulation often fail spectacularly in the real world — not because they lack intelligence, but because reality is harsher, rarer, and more adversarial than anything they prepared for. This talk presents a unified research programme at the intersection of formal verification, optimization, and reinforcement learning that asks a simple but far-reaching question: how do we build agents that come with mathematical safety guarantees, even when the environment shifts beneath them or actively works against them? We show how ideas from risk theory and distributionally robust optimization yield certificates of robustness that quantify exactly how much environmental uncertainty a policy can tolerate, and introduce scalable algorithms that bypass expensive classical computations to make these guarantees tractable and verifiable in complex settings.
Abstract
Machine learning models are increasingly deployed in safety-critical applications, yet they remain highly vulnerable to adversarial manipulation. Small but carefully crafted perturbations can be introduced either during training, through data poisoning, or at deployment, through evasion attacks, resulting in significant performance degradation and potentially unsafe behavior. This challenge raises a fundamental question: how can one provide formal guarantees that a learned model will remain reliable in the presence of such adversarial perturbations? In this talk, we present a unified robustness certification framework for neural networks by reformulating this robustness problem as a safety verification problem in control theory. In particular, we show how robustness against both train-time and test-time attacks can be analyzed through a systems-theoretic perspective, which enables the use of powerful verification tools from control. This viewpoint not only provides a principled and interpretable foundation for certification, but also offers several conceptual and technical advantages over existing robustness certification approaches by leveraging the structure and guarantees naturally available in dynamical systems and control-theoretic analysis.
Abstract
For interpretability and formal verification of neural networks, it is often desirable to extract finite-state automata from trained neural networks to gain a more tangible representation of the learned language. To this end, variants of Angluin's L* algorithm are widely employed. In its original formulation, the L* algorithm constructs a hypothesis automaton by interacting with an oracle through two types of queries: membership queries and equivalence queries. When a neural network serves as the oracle, equivalence queries cannot be applied in their original form, as this requires access to a ground-truth automaton for checking equivalence with the hypothesis automaton. As a result, many alternatives to the original equivalence queries have been proposed. This talk provides an overview of existing approaches and discusses their strengths and weaknesses
Abstract
Abstract interpretation is a method to effectively compute program invariants that possibly guarantee absence of certain runtime failures such as division by 0, null pointer dereferences or buffer overruns. After a smooth introduction to the underlying ideas and constructions, this tutorial shows by example how instrumentation of the code in combination with relational analysis may significantly enhance the expressiveness of inferred invariants.
Abstract
In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic, and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This talk will present version 1.0 of the SV-LIB format, including its design goals, its syntax, and informal semantics. In addition, we will mention some of the tools that already support SV-LIB and outline future plans for the format.