FORMAL VERIFICATION OF THE IEEE FLOATING-POINT TYPE IN BOOGIE AND SMACK
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.
Keywords
Authors who submit to this journal must agree to the following terms:
a) Authors retain copyright over their work, while allowing the conference to place this unpublished work under a Creative Commons Attribution License, which allows others to freely access, use, and share the work, with an acknowledgement of the work's authorship and its initial presentation at this conference.
b) Authors are able to waive the terms of the CC license and enter into separate, additional contractual arrangements for the non-exclusive distribution and subsequent publication of this work (e.g., publish a revised version in a journal, post it to an institutional repository or publish it in a book), with an acknowledgement of its initial presentation at this conference.
c) In addition, authors are encouraged to post and share their work online (e.g., in institutional repositories or on their website) at any point before and after the conference.
d) The Author grants Marriott Library the nonexclusive, perpetual, worldwide, irrevocable right to reproduce, distribute, display, publish, archive, preserve, digitize, transcribe, translate, provide access and transmit their work (in whole or in part) for any non-commercial purpose including but not limited to archiving, academic research, and marketing in such tangible electronic formats as may be in existence now or hereafter developed.
e) Marriott Library may elect, in its sole discretion, not to exercise the rights granted herein.
f) Author shall retain copyright in and to the Work and Marriott Library shall provide proper attribution in its exercise of the rights granted herein.
g) Author is solely responsible and will indemnify and hold Marriott Library and/or the University of Utah harmless for any third party claims related to the Work as submitted for publication.
