Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
Verifying Device Drivers with Pancake
Junming Zhao, Miki Tanaka, Johannes Åman Pohjola +10
Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant d…
cs.PL2017
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Heiko Becker, Nikita Zyuzin, Raphael Monat +3
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 discrepa…