Laura Titolo: ReFlow: from real number specifications to floating-point number implementations

Writing floating-point code is challenging. Due to the presence of round-off errors and runtime exceptions, certain properties that intuitively hold assuming exact real number arithmetics, no longer hold when using floating-point arithmetic. This talk presents ReFlow, a tool that automatically generates a floating-point C implementation from a PVS real number specification. ReFlow annotates the code with ACSL contracts stating the accumulated round-off error and it performs an instrumentation to detect when the floating-point control flow may diverge with respect to the ideal one. This generated code can be formally proven correct with a combination of the FramaC analyzer and the PVS theorem prover. ReFlow has been applied for generating code for the DAIDALUS NASA Library for air traffic collision detection and avoidance.

Aditya Thakur: Towards Provable Neurosymbolic Training of Deep Neural Networks for Scientific Machine Learning

The need for correctness of Deep neural networks (DNNs) used in applications such as image recognition and autonomous-vehicle control is well recognized. Correctness is expressed pointwise via specific input-output data or symbolically using robustness constraints and other safety specifications. In this talk, we will look at the problem of provable neurosymbolic training of DNNs in the context of scientific machine learning: the goal is to train a DNN using data along with physics-informed constraints so that the trained DNN is guaranteed to satisfy the given constraints. The talk will discuss how recent techniques for the provable repair of DNNs can be adapted to this problem of provable training as well as some of the challenges involved.