Polynomial function intervals for floating-point software verification

Jan Duracz*, Michal Konečný

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


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
Issue number4
Publication statusPublished - 24 Apr 2014

Bibliographical note

The original publication is available at www.springerlink.com

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


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


Dive into the research topics of 'Polynomial function intervals for floating-point software verification'. Together they form a unique fingerprint.

Cite this