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

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.