6 papers
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos +2
Neural networks have emerged as essential components in safety-critical applications -- these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNN…
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Magnus O. Myreen, Mario Carneiro
Conway's Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete…
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…
Formally Certified Approximate Model Counting
Yong Kiam Tan, Jiong Yang, Mate Soos +2
Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunct…
Clocked Definitions in HOL
Ramana Kumar, Magnus O. Myreen
Many potentially non-terminating functions cannot be directly defined in a logic of total functions, such as HOL. A well-known solution to this is to define non-terminating functio…
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…