iiinova — where your digital self keeps evolving

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 · 17/04/2026

Our paper on Heterogeneous Dynamic Logic has been accepted at #PLDI 2026 🥳 HDL lets you reason about systems mixing different computational models (in Cyber-Physical Systems and beyond) while *reusing* existing proof infrastructure for homogeneous subsystems. Preprint: arxiv.org/abs/2507.08581

arxiv.org

Heterogeneous Dynamic Logic: Provability Modulo Program Theories

Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for comb...

010

Samuel Teuber @ PLDI @teuber.bsky.social · 23/03/2026

I‘m excited to present my work on Provably Safe Neural Network Control at @horizonomega.org‘s Guaranteed Safe AI online seminar on April 9th. The talk will based on my NeurIPS‘24 paper with some updates on what I’ve been up to since :) Feel free to join if you’re interested:

142

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 · 22/12/2024

Our paper on confidence-based equivalence verification of NNs has just been accepted to #TACAS25 🥳 I'm looking forward to present our new Zonotope-based abstract domain -- we also explored which equivalence properties are more/less amenable to differential verification... teuber.dev/publication/...

teuber.dev

Revisiting Differential Verification: Equivalence Verification with Confidence | Samuel Teuber

We introduce a new abstract domain for differential verification using Zonotopes and explore which equivalence properties are ammenable to differential verification. Furthermore, we propose an improve...

050

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

If you're at #NeurIPS this week: I'm organising a "Formal Methods and AI" dinner on Saturday evening. You can find the details in the Whova App (-> Meet-ups -> Formal Methods and AI Dinner).

061

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

If you want to learn more about steering Cyber-Physical Systems with Neural Networks and *without* crashes, visit my #NeurIPS poster 4201 Thursday afternoon!

041

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

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

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

Hello everyone! I'm giving this platform a shot now after what Twitter has become...

020