The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems

TitleThe {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems
Publication TypeJournal Article
Year of Publication2008
AuthorsBagnara R, Hill PM, Zaffanella E
JournalScience of Computer Programming
Volume72
Pagination3–21
ISSN0167-6423
Keywordsabstract interpretation, computer-aided verification, formal methods, numerical properties, software verification, static analysis
Abstract

Since its inception as a student project in 2001, initially just for the handling (as the name implies) of convex polyhedra, the Parma Polyhedra Library has been continuously improved and extended by joining scrupulous research on the theoretical foundations of (possibly non-convex) numerical abstractions to a total adherence to the best available practices in software development. Even though it is still not fully mature and functionally complete, the Parma Polyhedra Library already offers a combination of functionality, reliability, usability and performance that is not matched by similar, freely available libraries. In this paper, we present the main features of the current version of the library, emphasizing those that distinguish it from other similar libraries and those that are important for applications in the field of analysis and verification of hardware and software systems.

DOI10.1016/j.scico.2007.08.001
File attachments: 

An Improved Tight Closure Algorithm for Integer Octagonal Constraints

TitleAn Improved Tight Closure Algorithm for Integer Octagonal Constraints
Publication TypeConference Paper
Year of Publication2008
AuthorsBagnara R, Hill PM, Zaffanella E
EditorLogozzo F, Peled D, Zuck L
Conference NameVerification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008)
PublisherSpringer Berlin / Heidelberg
Conference LocationSan Francisco, CA, USA
ISBN Number3-540-78162-2
Keywordsabstract interpretation, numerical properties, software verification, static analysis, unit two variables per inequality integer constraints, UTVPI integer constraints
Abstract

Integer octagonal constraints(a.k.a.\ Unit Two Variables Per Inequality or UTVPI integer constraints) constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and formal analysis and verification of software and hardware systems, since they couple algorithms having polynomial complexity with a relatively good expressive power. The main algorithms required for the manipulation of such constraints are the satisfiability check and the computation of the inferential closure of a set of constraints. The latter is called tight closure to mark the difference with the (incomplete) closure algorithm that does not exploit the integrality of the variables. In this paper we present and fully justify an O(n^3) algorithm to compute the tight closure of a set of UTVPI integer constraints.

DOI10.1007/978-3-540-78163-9_6
File attachments: 

Grids: A Domain for Analyzing the Distribution of Numerical Values

TitleGrids: A Domain for Analyzing the Distribution of Numerical Values
Publication TypeConference Paper
Year of Publication2007
AuthorsBagnara R, Dobson K, Hill PM, Mundell M, Zaffanella E
EditorPuebla G
Conference NameLogic-based Program Synthesis and Transformation, 16th International Symposium
PublisherSpringer-Verlag, Berlin
Conference LocationVenice, Italy
ISBN Number3-540-71409-X
Keywordsabstract interpretation, congruences, numerical abstraction, numerical properties, software verification, static analysis
Abstract

This paper explores the abstract domain of grids, a domain that is able to represent sets of equally spaced points and hyperplanes over an $n$-dimensional vector space. Such a domain is useful for the static analysis of the patterns of distribution of the values program variables can take. We present the domain, its representation and the basic operations on grids necessary to define the abstract semantics. We show how the definition of the domain and its operations exploit well-known techniques from linear algebra as well as a dual representation that allows, among other things, for a concise and efficient implementation.

DOI10.1007/978-3-540-71410-1_16
File attachments: 

Verification of {C} Programs Via Natural Semantics and Abstract Interpretation

TitleVerification of {C} Programs Via Natural Semantics and Abstract Interpretation
Publication TypeConference Paper
Year of Publication2007
AuthorsBagnara R, Hill PM, Pescetti A, Zaffanella E
EditorTews H
Conference NameProceedings of the C/C++ Verification Workshop
Conference LocationOxford, UK
Keywordsabstract interpretation, software verification, static analysis, structured operational semantics

Deriving Escape Analysis by Abstract Interpretation

TitleDeriving Escape Analysis by Abstract Interpretation
Publication TypeJournal Article
Year of Publication2006
AuthorsHill PM, Spoto F
JournalHigher-Order and Symbolic Computation
Volume19
Pagination415–463
ISSN1388-3690
Keywordsabstract interpretation, escape analysis, Java, object-oriented languages, software verification, static analysis
Abstract

Escape analysis of object-oriented languages determines, for every program point, the creation points of the objects reachable from the variables. This information allows us to stack allocate dynamically created objects and to reduce the overhead of synchronisation in Java-like languages. In this paper, we formalise the escape property E, computed by an escape analysis, as an abstract interpretation of concrete states. We show that it interacts with the static type information and with the late-binding mechanism. A static analysis based on the domain E can only be very imprecise. Therefore, we define a refinement ER of E, in the sense that ER is more concrete than E and, hence, leads to a more precise escape analysis than E. Our implementation of ER is a formally correct escape analyser, able to detect the stack allocatable creation points of middle-size Java (bytecode) applications.

DOI10.1007/s10990-006-0481-5

Widening Operators for Powerset Domains

TitleWidening Operators for Powerset Domains
Publication TypeJournal Article
Year of Publication2006
AuthorsBagnara R, Hill PM, Zaffanella E
JournalSoftware Tools for Technology Transfer
Volume8
Pagination449–466
ISSN1433-2779
Keywordsabstract interpretation, convex polyhedra, disjunctive refinement, finite powerset construction, powersets, software verification, static analysis, widening
Abstract

The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. While most of the operations on the finite powerset abstract domain are easily obtained by ‘‘lifting’’ the corresponding operations on the base-level domain, the problem of endowing finite powersets with a provably correct widening operator is still open. In this paper we define three generic widening methodologies for the finite powerset abstract domain. The widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators that allow all the flexibility required to tune the complexity/precision trade-off. As far as we know, this is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. We illustrate the proposed techniques by instantiating our widening methodologies on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

DOI10.1007/s10009-005-0215-8
File attachments: 

cTI: A Constraint-Based Termination Inference Tool for {ISO-Prolog}

TitlecTI: A Constraint-Based Termination Inference Tool for {ISO-Prolog}
Publication TypeJournal Article
Year of Publication2005
AuthorsMesnard F, Bagnara R
JournalTheory and Practice of Logic Programming
Volume5
Pagination243–257
ISSN1471-0684
Keywordsabstract interpretation, logic programming, software verification, static analysis, termination analysis, termination inference
Abstract

We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.

DOI10.1017/S1471068404002017
File attachments: 

Enhanced Sharing Analysis Techniques: A Comprehensive Evaluation

TitleEnhanced Sharing Analysis Techniques: A Comprehensive Evaluation
Publication TypeJournal Article
Year of Publication2005
AuthorsBagnara R, Zaffanella E, Hill PM
JournalTheory and Practice of Logic Programming
Volume5
Pagination1-43
ISSN1471-0684
Keywordsabstract interpretation, experimental evaluation, logic programming, sharing analysis, software verification, static analysis
Abstract

Sharing, an abstract domain developed by D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the integration of Sharing with freeness and linearity information, can significantly improve the precision of the analysis. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper we experimentally evaluate: helping Sharing with the definitely ground variables found using Pos, the domain of positive Boolean formulas; the incorporation of explicit structural information; a full implementation of the reduced product of Sharing and Pos; the issue of reordering the bindings in the computation of the abstract mgu; an original proposal for the addition of a new mode recording the set of variables that are deemed to be ground or free; a refined way of using linearity to improve the analysis; the recovery of hidden information in the combination of Sharing with freeness information. Finally, we discuss the issue of whether tracking compoundness allows the computation of more sharing information.

DOI10.1017/S1471068404001978
File attachments: 

Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra

TitleGeneration of Basic Semi-algebraic Invariants Using Convex Polyhedra
Publication TypeConference Paper
Year of Publication2005
AuthorsBagnara R, Rodríguez-Carbonell E, Zaffanella E
EditorHankin C, Siveroni I
Conference NameStatic Analysis: Proceedings of the 12th International Symposium
PublisherSpringer-Verlag, Berlin
Conference LocationLondon, UK
ISBN Number3-540-28584-9
Keywordsabstract interpretation, nonlinear invariants, numerical properties, software verification, static analysis
Abstract

A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined by conjunctions of polynomial inequalities, by means of convex polyhedra. While improving on the existing methods for generating invariant polynomial \emph{equalities}, since polynomial inequalities are allowed in the guards of the transition system, the approach does not suffer from the prohibitive complexity of the methods based on quantifier-elimination. The application of our implementation to benchmark programs shows that the method produces non-trivial invariants in reasonable time. In some cases the generated invariants are essential to verify safety properties that cannot be proved with classical linear invariants.

DOI10.1007/11547662_4
File attachments: 

Not Necessarily Closed Convex Polyhedra and the Double Description Method

TitleNot Necessarily Closed Convex Polyhedra and the Double Description Method
Publication TypeJournal Article
Year of Publication2005
AuthorsBagnara R, Hill PM, Zaffanella E
JournalFormal Aspects of Computing
Volume17
Pagination222–257
ISSN0934-5043
Keywordsabstract interpretation, convex polyhedra, double description method, minimization, numerical properties, software verification, static analysis
Abstract

Since the seminal work of Cousot and Halbwachs, the domain of convex polyhedra has been employed in several systems for the analysis and verification of hardware and software components. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a higher dimensional vector space and reuse the tools and techniques already available for closed polyhedra. In this work we highlight and discuss the issues underlying such an embedding for those implementations that are based on the double description method, where a polyhedron may be described by a system of linear constraints or by a system of generating rays and points. Two major achievements are the definition of a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.

DOI10.1007/s00165-005-0061-1
File attachments: