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

Junaid Rasheed; Michal Konečný

doi:10.1007/978-3-031-17108-6_2

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

Junaid Rasheed, Michal Konečný

Research output: Chapter in Book/Published conference output › Conference 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 language	English
Title of host publication	Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings
Editors	Bernd-Holger Schlingloff, Ming Chai
Pages	20-36
ISBN (Electronic)	978-3-031-17108-6
DOIs	https://doi.org/10.1007/978-3-031-17108-6_2
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 https://sefm-conference.github.io/2022/

Publication series

Name	Lecture Notes in Computer Science
Volume	13550

Conference

Conference	20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings
Abbreviated title	SEFM
Country/Territory	Germany
City	Berlin
Period	26/09/22 → 30/09/22
Internet address	https://sefm-conference.github.io/2022/

Keywords

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

Access to Document

10.1007/978-3-031-17108-6_2

Cite this

@inproceedings{ca5c19c13629486ba0f4d72add457c86,

title = "Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers",

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.",

keywords = "Automated proving, Floating-point computation, Interval methods, Software assurance, Software verification",

author = "Junaid Rasheed and Michal Kone{\v c}n{\'y}",

year = "2022",

month = oct,

day = "1",

doi = "10.1007/978-3-031-17108-6_2",

language = "English",

isbn = "978-3-031-17107-9",

series = "Lecture Notes in Computer Science",

pages = "20--36",

editor = "Bernd-Holger Schlingloff and Ming Chai",

booktitle = "Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings",

note = "20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings, SEFM ; Conference date: 26-09-2022 Through 30-09-2022",

url = "https://sefm-conference.github.io/2022/",

}

Rasheed, J & Konečný, M 2022, Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers. in B-H Schlingloff & M Chai (eds), Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings. Lecture Notes in Computer Science, vol. 13550, pp. 20-36, 20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings, Berlin, Germany, 26/09/22. https://doi.org/10.1007/978-3-031-17108-6_2

Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers. / Rasheed, Junaid; Konečný, Michal.
Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings. ed. / Bernd-Holger Schlingloff; Ming Chai. 2022. p. 20-36 (Lecture Notes in Computer Science; Vol. 13550).

Research output: Chapter in Book/Published conference output › Conference publication

TY - GEN

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

AU - Rasheed, Junaid

AU - Konečný, Michal

PY - 2022/10/1

Y1 - 2022/10/1

N2 - 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.

AB - 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.

KW - Automated proving

KW - Floating-point computation

KW - Interval methods

KW - Software assurance

KW - Software verification

UR - https://link.springer.com/chapter/10.1007/978-3-031-17108-6_2

UR - http://www.scopus.com/inward/record.url?scp=85140444038&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-17108-6_2

DO - 10.1007/978-3-031-17108-6_2

M3 - Conference publication

SN - 978-3-031-17107-9

T3 - Lecture Notes in Computer Science

SP - 20

EP - 36

BT - Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings

A2 - Schlingloff, Bernd-Holger

A2 - Chai, Ming

T2 - 20th International Conference, S0ftware Engineering and Formal Methods 2022 Berlin, Germany, September 26–30, 2022 Proceedings

Y2 - 26 September 2022 through 30 September 2022

ER -

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

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Automatic Numerical Solving for Auto-active Verification of Floating-Point Programs

Cite this

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

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Student theses

Automatic Numerical Solving for Auto-active Verification of Floating-Point Programs

Cite this