Sam Pollard on Verifying FP in C @ FPBench Community Meeting on April 6, 9am PT

[Zachary Tatlock]

Howdy folks!

Next Thursday, April 6, Sam Pollard from Sandia will be presenting in our monthly FPBench Community meeting at 9am PT!

Zoom: https://washington.zoom.us/j/92831331326

Formal and Semi-Formal Verification of Floating-Point Computations in C Programs

Abstract: For better or worse, the world runs on C, and to a lesser extent, C with IEEE 754 floating point. At Sandia Labs, we often are tasked with the formal verification of high-consequence programs in C. Two methods we use at Sandia to accomplish this verification are: fully constructive proofs of correctness (in the Coq theorem prover), and deductive verification (using Frama-C). In both cases, the addition of numerical computations adds complexity to the programs, via numerical error (e.g., discretization or roundoff error), or run-time errors (such as floating-point exceptions). We discuss our efforts at Sandia Labs to both make numerical models of C programs using Frama-C and its ANSI C specification language (ACSL), as well as functional models in Coq, and how to check whether the relevant C code implements these specifications.


Bio: Sam Pollard is a senior R&D scientist at Sandia National Laboratories in Livermore, California. Sam grew up in the pacific northwest and received his Ph.D. in computer science from the University of Oregon in 2021. His research focuses on the formal verification of high-consequence systems. He works to verify these systems using state machine models or machine-checkable proofs. He also designs tools which help verify systems wherein low-level implementation details can cause subtle bugs, such as the tricky semantics of C or floating-point computations.

Super stoked for this talk and to see y'all!

Best regards,

Z