×

Relational abstract domains for the detection of floating-point run-time errors. (English) Zbl 1126.68353

Schmidt, David (ed.), Programming languages and systems. 13th European symposium on programming, ESOP 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21313-9/pbk). Lecture Notes in Computer Science 2986, 3-17 (2004).
Summary: We present a new idea to adapt relational abstract domains to the analysis of IEEE 754-compliant floating-point numbers in order to statically detect, through Abstract Interpretation-based static analyses, potential floating-point run-time exceptions such as overflows or invalid operations. In order to take the non-linearity of rounding into account, expressions are modeled as linear forms with interval coefficients. We show how to extend already existing numerical abstract domains, such as the octagon abstract domain, to efficiently abstract transfer functions based on interval linear forms. We discuss specific fixpoint stabilization techniques and give some experimental results.
For the entire collection see [Zbl 1046.68014].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65G40 General methods in interval analysis

Software:

PPL
PDFBibTeX XMLCite
Full Text: DOI