Foundations and Trends® in Programming Languages > Vol 4 > Issue 3-4

Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation

By Antoine Miné, Sorbonne Universités, UPMC Univ. Paris 06, CNRS, LIP6, France, antoine.mine@lip6.fr

 
Suggested Citation
Antoine Miné (2017), "Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation", Foundations and Trends® in Programming Languages: Vol. 4: No. 3-4, pp 120-372. http://dx.doi.org/10.1561/2500000034

Publication Date: 05 Dec 2017
© 2017 A. Miné
 
Subjects
Abstract Interpretation,  Program Verification,  Static and Dynamic Program Analysis
 

Free Preview:

Download extract

Share

Download article
In this article:
1. Introduction
2. Elements of Abstract Interpretation
3. Language and Semantics
4. Non-Relational Abstract Domains
5. Relational Abstract Domains
6. Domain Transformers
7. Conclusion
Acknowledgements
References

Abstract

Born in the late 70s, Abstract Interpretation has proven an effective method to construct static analyzers. It has led to successful program analysis tools routinely used in avionic, automotive, and space industries to help ensuring the correctness of mission-critical software. This tutorial presents Abstract Interpretation and its use to create static analyzers that infer numeric invariants on programs. We first present the theoretical bases of Abstract Interpretation: how to assign a well-defined formal semantics to programs, construct computable approximations to derive effective analyzers, and ensure soundness, i.e., any property derived by the analyzer is true of all actual executions — although some properties may be missed due to approximations, a necessary compromise to keep the analysis automatic, sound, and terminating when inferring uncomputable properties.We describe the classic numeric abstractions readily available to an analysis designer: intervals, polyhedra, congruences, octagons, etc., as well as domain combiners: the reduced product and various disjunctive completions. This tutorial focuses not only on the semantic aspect, but also on the algorithmic one, providing a description of the data-structures and algorithms necessary to effectively implement all our abstractions. We will encounter many trade-offs between cost on the one hand, and precision and expressiveness on the other hand. Invariant inference is formalized on an idealized, toy-language, manipulating perfect numbers, but the principles and algorithms we present are effectively used in analyzers for real industrial programs, although this is out of the scope of this tutorial. This tutorial is intended as an entry course in Abstract Interpretation, after which the reader should be ready to read the research literature on current advances in Abstract Interpretation and on the design of static analyzers for real languages.

DOI:10.1561/2500000034
ISBN: 978-1-68083-386-7
267 pp. $99.00
Buy book (pb)
 
ISBN: 978-1-68083-387-4
267 pp. $260.00
Buy E-book (.pdf)
Table of contents:
1. Introduction
2. Elements of Abstract Interpretation
3. Language and Semantics
4. Non-Relational Abstract Domains
5. Relational Abstract Domains
6. Domain Transformers
7. Conclusion
Acknowledgements
References

Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation

This monograph presents Abstract Interpretation and its use to create static analyzers that infer numeric properties on programs. Abstract Interpretation, born in the late 1970s, has proven a very effective method to construct static analyzers. It has led to successful program analysis tools like PolySpace Verifier (The Mathworks) and the Astrée analyzer (AbsInt): industrial tools that are routinely used in the avionic, automotive, and space industries to help ensure the correctness of mission-critical software. Automatically inferring numeric invariants can be used to prove the absence of run-time errors, such as arithmetic overflows and out-of-bound array accesses, before the program is even run, while achieving a full coverage of the control and data space.

This monograph is based on several Master-level courses in Abstract Interpretation given by the author. It is intended as an entry course in Abstract Interpretation, after which the reader should be ready to read the research literature on current advances in Abstract Interpretation, as well as more practical articles on the design of industrial-strength static analyzers for real languages.

 
PGL-034