Samuel Teuber @ PLDI

@teuber.bsky.social

158 Followers 600 Following

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

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.
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"
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.
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.
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.