FORMAL VERIFICATION OF THE IEEE FLOATING-POINT TYPE IN BOOGIE AND SMACK

  • Dietrich Geisler University of Utah

Abstract

Throughout academia and industry, formal verification techniques have become essential for asserting code correctness and identifying potential bugs. Despite the growth of this field, however, there exists relatively few verifiers that can reason about the floating-point type. Since many areas of study involve code that relies on the correctness of the floating-point type, the lack of verifiers which can reason about the floating-point type is a cause for concern.The project presented here seeks to introduce the floating-point data type to the Boogie language and implement support for evaluating floating-points using the Boogie and SMACK tools. The addition of the floating-point type to Boogie allows mathematical reasoning about the floating-point type in the context of the Boogie type system and prover, including analysis of floating-points of arbitrary exponent and significand size. The subsequent addition of the floating-point type to SMACK allows the reasoning of floating-points in the C language, including reasoning about memory safety and parallelization through the SMACK evaluation framework. 

Author Biography

Dietrich Geisler, University of Utah
Senior Undergraduate Student.  Will be graduating in Computer Science, Applied Mathematics, and Physical/Mathematical Chemistry.
Published
2017-06-08
How to Cite
GEISLER, Dietrich. FORMAL VERIFICATION OF THE IEEE FLOATING-POINT TYPE IN BOOGIE AND SMACK. Undergraduate Research Journal, [S.l.], june 2017. Available at: <http://epubs.utah.edu/index.php/URJ/article/view/3901>. Date accessed: 22 oct. 2017.
Issue
Section
College of Engineering

Keywords

Verification, Floating-Points, SMACK