Polynomial function intervals for floating-point software verification

Research output: Contribution to journalArticle

View graph of relations Save citation

Open

Authors

Research units

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.

Documents

Details

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

Bibliographic 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

Download statistics

No data available

Employable Graduates; Exploitable Research

Copy the text from this field...