iiinova — where your digital self keeps evolving

Samuel Teuber @ PLDI

@teuber.bsky.social

159 followers 601 following 25 posts

Doctoral Researcher at KIT's Computer Science Department | Formal Methods for Software & AI (Focus on CPS and Fairness Verification) Currently migrating from Twitter (@teuber_dev) www.teuber.dev

Posts Replies Media

Samuel Teuber @ PLDI @teuber.bsky.social · 16/06/2026

I am at #PLDI where I will present work on heterogeneous systems verification on Friday: Inspired by Satisfiability Modulo Theories we propose a framework for the combination of program logics while reusing proof infrastructure. Below a peak of some slides Details: pldi26.sigplan.org/details/pldi...

Heterogeneous Dynamic Theories combine multiple dynamic theories into one. By combining heterogeneous theories with lifting we receive dynamic theories that can express complex, interleaved heterogeneous behavior.

The features of a dynamic theory can be extended by lifting which takes a given dynamic theory, amends it features and calculus and gives us a new dynamic theory.

Our case study verifies a Java controller that steers a car in an environment modeled in differential dynamic logic.

010

Samuel Teuber @ PLDI @teuber.bsky.social · 09/05/2025

Thank you @etapsconf.bsky.social for the great event — so many interesting talks and discussions at #etaps this year! I also had the opportunity to present my #tacas paper on verifying behavioral equivalence of neural networks 😃

Me standing in the front of a lecture hall at McMaster University during the ETAPS conference: The slides read "Revisiting Differential Verification: Equivalence Verification with Confidence"

020

Samuel Teuber @ PLDI @teuber.bsky.social · 08/12/2024

This is really cool! I'm obviously nitpicking here, but I think it's very meta that quite a few papers on Neural Network Verification are right around the "decision boundary" of the Adversarial Robustness cluster...

020

Samuel Teuber @ PLDI @teuber.bsky.social · 17/11/2024

Perfection

030

Samuel Teuber @ PLDI @teuber.bsky.social · 17/11/2024

We applied the overall approach to multiple case studies including Vertical Airborne Collision Avoidance (VCAS): Here, we analyzed NNs from prior work and found numerous concrete safety problems -- but see for yourself (any plane trajectory in the red region is BAD!):

Six examples of the following:
A schematic plot of two planes flying towards each other at equal vertical positions. An orange line indicates the original flight trajectory of the plane on the left, and a blue line indicates an updated trajectory that was proposed by a neural network. The latter would lead to a crash of the two planes or at the very least ot a Near Mid Air Collision.

100

Samuel Teuber @ PLDI @teuber.bsky.social · 17/11/2024

We start with a dL safety proof for an abstract control envelope. Our approach then derives an NN specification. We rigorously define the NN's semantics in dL via "nondeterministic mirrors". Verification of the NN is then mirrored by a proof of infinite-time safety in dL.

An overview of the safety guarantee provided by our approach:
We start off with a provably safe control envelope (upper right) and a neural network (lower left). Our objective is to prove the safety of a neural network control system. By encoding the neural network as a program in differential dynamic logic, we derive the program for which we would like to prove safety (lower right). However, reasoning about this program directly is infeasible due to the subsymbolic reasoning of NNs. Instead, we derive a specification for the NN in isolation based on the provably safe control envelope (upper left). By verifying this specification, we simultaneously perform a refinement proof which shows that the neural network control system is safe.

100

Samuel Teuber @ PLDI @teuber.bsky.social · 17/11/2024

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

A schematic plot of two planes flying towards each other at equal vertical positions. An orange line indicates the original flight trajectory of the plane on the left, and a blue line indicates an updated trajectory that was proposed by a neural network. The latter would lead to a crash of the two planes.

1135