The International Conference for High Performance Computing, Networking, Storage, and Analysis
The International Conference for High Performance Computing, Networking, Storage, and Analysis
Workshop: Reasoning about Floating Point in the Real World
Abstract: The formal verification of floating point code as it exists in widely-used, highly-optimized libraries is very challenging, in fact so challenging that formal proofs, where they exist, are done manually. This talk will discuss a combination of recent results that allow some important codes to be verified fully automatically, as well as additional challenges that have yet to be overcome.