Machine Learning and Formal Methods

Topic: Machine Learning and Formal Methods

When: 10 June, 2026 

• Light lunch from 12.00 to 13.00 CET
• Presentations and discussions 13.00 to 17.00 CET

Where: E:1406, E-building LTH, Klas Anshelms väg 10 / Ole Römers väg 3, Lund, Sweden

Expected audience: The event is primarily aimed at researchers and professionals in the field.

Registration: To participate is free of charge. Welcome to sign up at ai.lu.se.

Host and moderator: Amir Aminifar, Senior lecturer, Secure and Networked Systems, Lund University

Speakers

• Prof. Yasser Shoukry, University of California, Irvine, USA
• Prof. Alessandro Biondi, Scuola Superiore Sant'Anna, Italy
• Dr. Caterina Urban, Inria & École Normale Supérieure | Université PSL, Paris, France
• Prof. Gerardo Schneider, Chalmers and the University of Gothenburg, Sweden

See agenda and abstracts below. 

Registration

To participate is free of charge. Sign up at ai.lu.se/2026-06-10b/registration.

Organisation

This event is organized as a WASP Lighthouse seminar in collaboration with AI Lund and ELLIIT 

Contact

• Amir Aminifar, Senior lecturer, Secure and Networked Systems, Lund University
• susanna [dot] lonnqvist [at] eit [dot] lth [dot] se (Susanna Lönnqvist), ELLIIT, Lund University
• Jonas Wisbrant, AI Lund

Agenda

• Lunch 12:00-13:00
• Opening the session 
• 13:00-13:40 Talk Yasser Shoukry
• 13:40-14:20 Talk Gerardo Schneider 
• 14:20-15:00 Fika
• 15:00-15:40 Panel discussion 
• 15:40-16:20 Talk Caterina Urban
• 16:20-17:00 Talk Alessandro Biondi
• Closing the session
   

Prof. Yasser Shoukry: Provably Safe Neural Architectures and Perception Pipelines Using Deep Bernstein Neural Networks 

Deep neural networks (DNNs) have fundamentally revolutionized autonomous and cyber-physical systems, yet their adoption in safety-critical domains remains limited due to their lack of rigorous, provable safety guarantees. Traditional verification approaches face an agonizing trade-off: complete verification techniques suffer from poor scalability, while incomplete approaches scale better but introduce loose, overly conservative bounds that rapidly degrade with network depth. 
  The first part of the talk focuses on DeepBern Networks—a promising alternative to traditional ReLU-based neural networks. By leveraging Bernstein polynomials as activation functions, we exploit their unique mathematical properties to develop a novel bound propagation algorithm (Bern-IBP) that delivers state-of-the-art certified accuracy. We also show that not only DeepBern Networks are easier to verify, but they also enjoy exponential approximation rates that are not attainable by ReLU-based networks. 
  The second part of the talk transitions from abstract networks to practical deployment, focusing on the formal verification of vision-based perception systems. We introduce a "correct-by-construction" framework for 3D pose estimation that fuses physics-driven geometric modeling with learning-based architectures. By embedding Geometric Generative Models (GGMs) directly into the image formation process and utilizing neural network reachability analysis, we show how an autonomous agent can retrieve tightly bounded, certified 3D pose estimates directly from event-based camera images of known environmental geometries (such as traffic signs or runway markings). 

Prof. Gerardo Schneider: Interest beyond Violation: On Points-of-Interest in Runtime Verification

 Many formal verification techniques are concerned with comparing system behaviours with formal specifications. Although runtime verification has followed this path (comparing observed traces against formal properties), it has traditionally been burdened with another task — that of raising a flag when a violation is detected. Different approaches can be found in the literature: identifying the earliest such instance, identifying all instances, identifying instances where (potentially future) violations are inevitable, etc. We argue that the lack of a clear distinction between the notion of system correctness and the hard-wired means of identification of points when violation is somehow detected, conflates the notions of points-of-detection and points-of-violation. Frequently, the point at which a point-of-violation may be detected is independent of the point of interest itself, and also independent of the point-of-reaction if a corrective measure is needed. We observe that this distinction becomes more salient in some cases, such as deontic specification languages, which may identify notions such as permission, and in the case of multi-agent systems, where the notion of blame is essential. 
  In this talk, I will give a number of examples to motivate why these limitations are significant for the field of runtime verification and suggest some research directions in the area. Joint work with Christian Colombo and Gordon Pace.

Dr. Caterina Urban: Verified Explanations of Neural Networks

Verified explanations offer a principled way to explain neural network decisions by grounding explainability in formally verified robustness, thereby addressing the inherently black-box nature of these models. We propose two complementary notions of verified explanations. The first is defined over the input space of neural networks, where we introduce hierarchical explanations, termed verifier-optimal robust explanations. These explanations explicitly account for the incompleteness of neural network verifiers, ensuring optimality with respect to the guarantees that can be formally established. The second notion is defined over the network’s internal (latent) representations, capturing explanations in terms of the model’s inner computations. We present novel efficient algorithms to compute both forms of explanations, and showcase their scalability and meaningfulness in practice. 

Dr. Alessandro Biondi: Secure Physical AI at the Edge: Virtualization, Isolation, and Trusted AI Execution for Cyber-Physical Systems

The increasing adoption of Physical AI in cyber-physical systems is driving the deployment of advanced AI capabilities directly on embedded edge platforms, where real-time constraints, safety requirements, and cybersecurity concerns must coexist. This talk discusses architectural and system-software technologies enabling the secure execution of AI workloads on heterogeneous embedded platforms operating in critical domains such as transportation, robotics, industrial automation, and aerospace.
  The presentation will introduce hypervisor-based virtualization and isolation mechanisms that allow multiple applications with different safety and security requirements to share the same hardware platform while maintaining strong separation and predictable behavior. It will then discuss approaches to protect AI-enabled systems against cyber attacks, including secure execution environments, runtime monitoring, and mechanisms to safeguard intellectual property by preventing AI model theft and unauthorized access to sensitive data.
  Finally, the talk will explore the concept of multi-enclave AI execution, where multiple AI models with different criticality, safety, and security levels can coexist on the same chip within isolated trusted domains. This approach enables the consolidation of heterogeneous workloads while preserving security, resilience, and certification requirements, paving the way toward trustworthy Physical AI at the edge.