Visible to the public Formal Verification of C Programs with Floating-Point Computations: Certified Error Bounds for Signal Processing

In this technical talk, I will present our results related to the certification of floating-point error bounds in C implementations of signal processing algorithms. In particular, this relates to the topic of reasoning about the uncertainty caused by the noise arising from floating-point rounding errors and approximate computations in C programs.