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.
|Title of host publication||Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings|
|Editors||Bernd-Holger Schlingloff, Ming Chai|
|Publication status||Published - 1 Oct 2022|
|Event||20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings - Berlin, Germany|
Duration: 26 Sept 2022 → 30 Sept 2022
|Name||Lecture Notes in Computer Science|
|Conference||20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings|
|Period||26/09/22 → 30/09/22|
- Automated proving
- Floating-point computation
- Interval methods
- Software assurance
- Software verification
FingerprintDive into the research topics of 'Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers'. Together they form a unique fingerprint.
Student thesis: Doctoral Thesis › Doctor of PhilosophyFile