BEGIN:VCALENDAR PRODID:-//eluceo/ical//2.0/EN VERSION:2.0 CALSCALE:GREGORIAN BEGIN:VEVENT UID:db27aaaa8a1894e3c0ccb06df76e1e93 DTSTAMP:20260714T070016Z SUMMARY:Machine Learning and Formal Methods DESCRIPTION:Contact: susanna.lonnqvist@eit.lth.se\n\nTopic: Machine Learnin g and Formal MethodsWhen: \;10 June\, 2026 \;Light lunch from 12.0 0 to 13.00 CETPresentations and discussions 13.00 to 17.00 CETWhere: \ ;E:1406\, E-building LTH\, Klas Anshelms väg 10 / Ole Römers väg 3\, Lu nd\, SwedenExpected audience: The event is primarily aimed at researchers and professionals in the field.Registration: To participate is free of cha rge. Welcome to sign up at ai.lu.se.Host and moderator: Amir Aminifar\, Se nior lecturer\, Secure and Networked Systems\, Lund UniversitySpeakersProf . Yasser Shoukry\, University of California\, Irvine\, USAProf. Alessandro Biondi\, Scuola Superiore Sant'Anna\, ItalyDr. Caterina Urban\, Inria &am p\; École Normale Supérieure | Université PSL\, Paris\, FranceProf. Ger ardo Schneider\, Chalmers and the University of Gothenburg\, SwedenSee age nda and abstracts below. \;RegistrationTo participate is free of charg e. Sign up at ai.lu.se/2026-06-10b/registration.OrganisationThis event is organized as a WASP Lighthouse seminar in collaboration with AI Lund and E LLIIT \;ContactAmir Aminifar\, Senior lecturer\, Secure and Networked Systems\, Lund UniversitySusanna Lönnqvist\, ELLIIT\, Lund UniversityJona s Wisbrant\, AI LundAgendaLunch 12:00-13:00Opening the session \;13:00 -13:40 Talk Yasser Shoukry13:40-14:20 Talk Gerardo Schneider \;14:20-1 5:00 Fika15:00-15:40 Panel discussion \;15:40-16:20 Talk Caterina Urba n16:20-17:00 Talk Alessandro BiondiClosing the session \;Prof. Yasser Shoukry: Provably Safe Neural Architectures and Perception Pipelines Using  \;Deep Bernstein Neural \;Networks \;Deep neural networks (DN Ns) have fundamentally revolutionized autonomous and cyber-physical system s\, yet their adoption in safety-critical domains remains limited due to t heir lack of rigorous\, provable safety guarantees. Traditional verificati on approaches face an agonizing trade-off: complete verification technique s 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 DeepBe rn Networks—a promising alternative to traditional ReLU-based neural net works. By leveraging Bernstein polynomials as activation functions\, we ex ploit their unique mathematical properties to develop a novel bound propag ation algorithm (Bern-IBP) that delivers state-of-the-art certified accura cy. We also show that not only DeepBern Networks are easier to verify\, bu t they also enjoy exponential approximation rates that are not attainable by ReLU-based networks. \; \; The second part of the talk transiti ons from abstract networks to practical deployment\, focusing on the forma l verification of vision-based perception systems. We introduce a "correct -by-construction" framework for 3D pose estimation that fuses physics-driv en geometric modeling with learning-based architectures. By embedding Geom etric Generative Models (GGMs) directly into the image formation process a nd utilizing neural network reachability analysis\, we show how an autonom ous agent can retrieve tightly bounded\, certified 3D pose estimates direc tly from event-based camera images of known environmental geometries (such as traffic signs or runway markings). \;Prof. Gerardo Schneider: Inte rest beyond Violation: On Points-of-Interest in Runtime Verification \ ;Many formal verification techniques are concerned with comparing system b ehaviours with formal specifications. Although runtime verification has fo llowed this path (comparing observed traces against formal properties)\, i t has traditionally been burdened with another task — that of raising a flag when a violation is detected. Different approaches can be found in th e literature: identifying the earliest such instance\, identifying all ins tances\, identifying instances where (potentially future) violations are i nevitable\, etc. We argue that the lack of a clear distinction between the notion of system correctness and the hard-wired means of identification o f points when violation is somehow detected\, conflates the notions of poi nts-of-detection and points-of-violation. Frequently\, the point at which a point-of-violation may be detected is independent of the point of intere st itself\, and also independent of the point-of-reaction if a corrective measure is needed. We observe that this distinction becomes more salient i n some cases\, such as deontic specification languages\, which may identif y notions such as permission\, and in the case of multi-agent systems\, wh ere the notion of blame is essential. \; \; In this talk\, I will give a number of examples to motivate why these limitations are significan t for the field of runtime verification and suggest some research directio ns in the area. Joint work with Christian Colombo and Gordon Pace.Dr. Cate rina Urban: Verified Explanations of Neural NetworksVerified explanations offer a principled way to explain neural network decisions by grounding ex plainability in formally verified robustness\, thereby addressing the inhe rently black-box nature of these models. We propose two complementary noti ons of verified explanations. The first is defined over the input space of neural networks\, where we introduce hierarchical explanations\, termed v erifier-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 secon d 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\, Isola tion\, and Trusted AI Execution for Cyber-Physical SystemsThe increasing a doption of Physical AI in cyber-physical systems is driving the deployment of advanced AI capabilities directly on embedded edge platforms\, where r eal-time constraints\, safety requirements\, and cybersecurity concerns mu st coexist. This talk discusses architectural and system-software technolo gies enabling the secure execution of AI workloads on heterogeneous embedd ed platforms operating in critical domains such as transportation\, roboti cs\, industrial automation\, and aerospace. \; The presentation will i ntroduce hypervisor-based virtualization and isolation mechanisms that all ow multiple applications with different safety and security requirements t o share the same hardware platform while maintaining strong separation and predictable behavior. It will then discuss approaches to protect AI-enabl ed 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.&nb sp\; Finally\, the talk will explore the concept of multi-enclave AI execu tion\, where multiple AI models with different criticality\, safety\, and security levels can coexist on the same chip within isolated trusted domai ns. This approach enables the consolidation of heterogeneous workloads whi le preserving security\, resilience\, and certification requirements\, pav ing the way toward trustworthy Physical AI at the edge.\n\nMore informatio n about the event: https://www.ai.lu.se/evenemang/machine-learning-and-for mal-methods DTSTART;TZID=GMT:20260610T100000 DTEND;TZID=GMT:20260610T150000 LOCATION:E:1406\, E-building LTH\, Klas Anshelms väg 10 /Ole Römers väg 10\, Lund\, Sweden END:VEVENT END:VCALENDAR