5 papers
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer +1
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL),…
An Information-Flow Perspective on Algorithmic Fairness
Samuel Teuber, Bernhard Beckert
This work presents insights gained by investigating the relationship between algorithmic fairness and the concept of secure information flow. The problem of enforcing secure inform…
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Samuel Teuber, Debasmita Lohar, Bernhard Beckert
As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes cruci…
Next Steps in LLM-Supported Java Verification
Samuel Teuber, Bernhard Beckert
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scalin…
Revisiting Differential Verification: Equivalence Verification with Confidence
Samuel Teuber, Philipp Kern, Marvin Janzen +1
When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To…