Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers

Junaid Rasheed, Michal Konečný

Research output: Chapter in Book/Published conference outputConference publication

Abstract

We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying SPARK programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings
EditorsBernd-Holger Schlingloff, Ming Chai
Pages20-36
ISBN (Electronic)978-3-031-17108-6
DOIs
Publication statusPublished - 1 Oct 2022
Event20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings - Berlin, Germany
Duration: 26 Sept 202230 Sept 2022
https://sefm-conference.github.io/2022/

Publication series

NameLecture Notes in Computer Science
Volume13550

Conference

Conference20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings
Abbreviated titleSEFM
Country/TerritoryGermany
CityBerlin
Period26/09/2230/09/22
Internet address

Keywords

  • Automated proving
  • Floating-point computation
  • Interval methods
  • Software assurance
  • Software verification

Fingerprint

Dive into the research topics of 'Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers'. Together they form a unique fingerprint.

Cite this