1

A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4

Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepancy between continuous reals and discrete finite-precision values, …

Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions

We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it …