Polynomial function intervals for floating-point software verification

Jan Duracz*, Michal Konečný

*Corresponding author for this work

Research output: Contribution to journalArticle

Abstract

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.

Original languageEnglish
Pages (from-to)351-398
Number of pages48
JournalAnnals of Mathematics And artificial Intelligence
Volume70
Issue number4
DOIs
Publication statusPublished - 24 Apr 2014

Fingerprint

Software Verification
Floating point
Polynomial function
Polynomials
Specification
Specifications
Interval
Specification languages
Specification Languages
Real variables
Polynomial approximation
Interval Arithmetic
Tool Support
Polynomial Approximation
Integral Operator
Scalability
Inclusion
Engineers
Software
Costs

Bibliographical note

The original publication is available at www.springerlink.com

Funding: Altran Praxis Ltd; EPSRC [EP/C01037X/1]

Keywords

  • floating-point software verification
  • interval arithmetic
  • non-linear numerical constraint solving
  • polynomial intervals
  • theorem proving
  • validated computation

Cite this

@article{3018eb9dc3bf4843a4a247f920be9f3c,
title = "Polynomial function intervals for floating-point software verification",
abstract = "The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.",
keywords = "floating-point software verification, interval arithmetic, non-linear numerical constraint solving, polynomial intervals, theorem proving, validated computation",
author = "Jan Duracz and Michal Konečn{\'y}",
note = "The original publication is available at www.springerlink.com Funding: Altran Praxis Ltd; EPSRC [EP/C01037X/1]",
year = "2014",
month = "4",
day = "24",
doi = "10.1007/s10472-014-9409-7",
language = "English",
volume = "70",
pages = "351--398",
journal = "Annals of Mathematics And artificial Intelligence",
issn = "1012-2443",
publisher = "Springer",
number = "4",

}

Polynomial function intervals for floating-point software verification. / Duracz, Jan; Konečný, Michal.

In: Annals of Mathematics And artificial Intelligence, Vol. 70, No. 4, 24.04.2014, p. 351-398.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Polynomial function intervals for floating-point software verification

AU - Duracz, Jan

AU - Konečný, Michal

N1 - The original publication is available at www.springerlink.com Funding: Altran Praxis Ltd; EPSRC [EP/C01037X/1]

PY - 2014/4/24

Y1 - 2014/4/24

N2 - The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.

AB - The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.

KW - floating-point software verification

KW - interval arithmetic

KW - non-linear numerical constraint solving

KW - polynomial intervals

KW - theorem proving

KW - validated computation

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

U2 - 10.1007/s10472-014-9409-7

DO - 10.1007/s10472-014-9409-7

M3 - Article

AN - SCOPUS:84901188918

VL - 70

SP - 351

EP - 398

JO - Annals of Mathematics And artificial Intelligence

JF - Annals of Mathematics And artificial Intelligence

SN - 1012-2443

IS - 4

ER -