2012 | OriginalPaper | Buchkapitel
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
verfasst von : Arnaud J. Venet
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The inference of linear inequality invariants among variables of a program plays an important role in static analysis. The polyhedral abstract domain introduced by Cousot and Halbwachs in 1978 provides an elegant and precise solution to this problem. However, the computational complexity of higher-dimensional convex hull algorithms makes it impractical for real-size programs. In the past decade, much attention has been devoted to finding efficient alternatives by trading expressiveness for performance. However, polynomial-time algorithms are still too costly to use for large-scale programs, whereas the full expressive power of general linear inequalities is required in many practical cases. In this paper, we introduce the gauge domain, which enables the efficient inference of general linear inequality invariants within loops. The idea behind this domain consists of breaking down an invariant into a set of linear relations between each program variable and all loop counters in scope. Using this abstraction, the complexity of domain operations is no larger than
O
(
kn
), where
n
is the number of variables and
k
is the maximum depth of loop nests. We demonstrate the effectiveness of this domain on a real 144K LOC intelligent flight control system, which implements advanced adaptive avionics.