The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems
Science of Computer ProgrammingPublished 27 April 2008
Roberto Bagnara, Patricia M. Hill, Enea Zaffanella
Citations466
SJR quartileQ3
SJR score0.43
SNIP1.23
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The main features of the current version of the Parma Polyhedra Library are presented, 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.
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.
Keywords
Computer ScienceEngineering
ScienceDynamic Programming
13,088 Citations1966Richard Bellman
The more the authors study the information processing aspects of the mind, the more perplexed and impressed they become, and it will be a very long time before they understand these processes sufficiently to reproduce them.
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Journal of the Operational Research SocietyInteger and Combinatorial Optimization
5,548 Citations1990H. P. Williams, George L. Nemhauser +1 more
Electronic Notes in Theoretical Computer ScienceConstructing Induction Rules for Deductive Synthesis Proofs
2,811 Citations2006Alan Bundy, Lucas Dixon +2 more
It is shown that a combination of rippling and the use of meta-variables as a least-commitment device can provide novelty in induction rule construction techniques that can introduce novel recursive structures.
Systematic design of program analysis frameworks
1,598 Citations1979Patrick Cousot, Radhia Cousot
The systematic and correct design of program analysis frameworks with respect to a formal semantics is devoted to the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
Automatic discovery of linear restraints among variables of a program
1,576 Citations1978Patrick Cousot, Nicolas Halbwachs
Imperative functional programming
1,235 Citations1993Simon Jones, Philip Wadler
A new model, based on monads, for performing input/output in a non-strict, purely functional language that is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language working and in-place array updates.
Bulletin of the London Mathematical SocietyINTEGER AND COMBINATORIAL OPTIMIZATION
1,042 Citations1989David Connolly
Convexity and Optimization in Finite Dimensions I
881 Citations1970Josef Stoer, Christoph Witzgall
Greenwood Publishing Group Inc. eBooksFormal Theories of the Commonsense World
760 Citations1985Jerry R. Hobbs, Robert C. Moore
Lecture notes in computer scienceTiming assumptions and verification of finite-state concurrent systems
728 Citations1990David L. Dill
A scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties is described, and it is conjecture that the method presented can be extended in this way.
Journal of Logic and ComputationAbstract Interpretation Frameworks
695 Citations1992Patrick Cousot, Radhia Cousot
ACM SIGPLAN NoticesA static analyzer for large safety-critical software
577 Citations2003Bruno Blanchet, Patrick Cousot +6 more
Artificial IntelligenceConstraint propagation with interval labels
525 Citations1987Ernest Davis
This paper determines the completeness and running time of constraint propagation for various kinds of labels and constraints in AI systems of various kinds.
Lecture notes in computer sciencePHAVer: Algorithmic Verification of Hybrid Systems Past HyTech
480 Citations2005Goran Frehse
Lecture notes in computer scienceDouble description method revisited
423 Citations1996Komei Fukuda, A. Prodon
This paper reinvestigate this method for enumerating all extreme rays of a general polyhedral cone in ℝd, introduces some new ideas for efficient implementations, and shows some empirical results indicating its practicality in solving highly degenerate problems.
Lecture notes in computer scienceComparing the Galois connection and widening/narrowing approaches to abstract interpretation
421 Citations2006Patrick Cousot, Radhia Cousot
The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices.
Lecture notes in computer scienceThe ASTREÉ Analyzer
388 Citations2005Patrick Cousot, Radhia Cousot +5 more
ASTREE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language, producing a correctness proof for complex software without any false alarm in a few hours of computation.
Formal Methods in System DesignVerification of Real-Time Systems using Linear Relation Analysis
260 Citations1997Nicolas Halbwachs, Yann-Erick Proy +1 more
An abstract interpretation of linear Relation Analysis is applied to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.
The octagon abstract domain
232 Citations2002Antoine Miné
The octagon abstract domain is presented, a relational numerical abstract domain for static analysis by abstract interpretation that was incorporated into the ASTRÉE industrial-strength static analyzer and was key in proving the absence of run-time errors in large critical embedded flight control software for Airbus planes.
Lecture notes in computer scienceScalable Analysis of Linear Systems Using Mathematical Programming
213 Citations2005Sriram Sankaranarayanan, Henny B. Sipma +1 more
The method generalizes similar analyses in the interval, octagon, and octahedra domains, without resorting to polyhedral manipulations, and demonstrates the performance of the method on some benchmark programs.
Parallel algorithms and applicationsA LIBRARY FOR DOING POLYHEDRAL OPERATIONS
203 Citations2000Doran Wilde
The design and implementation of a library of C-code procedures to perform operations on rational polyhedra to support intersection, union, difference, simplification in context, convex hull, affine image, affines preimage, and computation of dual forms is described.
Birkhäuser Basel eBooksA Revised Implementation of the Reverse Search Vertex Enumeration Algorithm
186 Citations2000David Avis
Birkhäuser Basel eBooksPolytopes — Combinatorics and Computation
182 Citations2000Ziegler, Günther M, Gil Kalai
Efficient verification of real-time systems: compact data structure and state-space reduction
180 Citations2002Kim G. Larsen, Fredrik Larsson +2 more
A compact data structure for representing clock constraints is presented, based on an O(n/sup 3/) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints.
ACM Transactions on Computer-Human InteractionThe Cassowary linear arithmetic constraint solving algorithm
178 Citations2001Greg J. Badros, Alan Borning +1 more
Cassowary is described---an incremental algorithm based on the dual simplex method, which can solve systems of constraints efficiently and is implemented as part of a constraint-solving toolkit.
Automating mimicry attacks using static binary analysis
178 Citations2005Christopher Kruegel, Engin Kirda +3 more
A novel technique to evade the extended detection features of state-of-the-art intrusion detection systems and reduce the task of the intruder to a traditional mimicry attack is presented.
Lecture notes in computer scienceVerification of linear hybrid systems by means of convex approximations
169 Citations1994Nicolas Halbwachs, Yann -Eric Proy +1 more
A new application of the abstract interpretation by means of convex polyhedra to a class of hybrid systems, i.e., systems involving both discrete and continuous variables, is presented.
A framework for numeric analysis of array operations
155 Citations2005Denis Gopan, Thomas Reps +1 more
This work presents a framework for analyzing array operations that is capable of capturing numeric properties of array elements and is able to establish that all array elements are initialized by an array-initialization loop, as well as to discover numeric constraints on the values of initialized elements.
Discrete & Computational GeometryPrimal—Dual Methods for Vertex and Facet Enumeration
141 Citations1998D. Bremner, K. Fukuda +1 more
The known polynomially solvable classes of polytopes are extended by looking at the dual problems by proposing a new class of algorithms that take advantage of this phenomenon.
Lecture notes in computer scienceStatic analysis of linear congruence equalities among variables of a program
138 Citations1991Philippe Granger
This paper is dedicated to the presentation of a new static analysis of programs conceived for discovering linear congruence equations satisfied by integer valued variables (or more generally by any set of integer values abstracted from a program).
Lecture notes in computer scienceDelay analysis in synchronous programs
135 Citations1993Nicolas Halbwachs
This work proposes to apply linear relation analysis to variables used to count delays in synchronous programs, and finds that the results can be applied to code optimization and to the verification of real-time properties of programs.
Lecture notes in computer sciencePossibly Not Closed Convex Polyhedra and the Parma Polyhedra Library
132 Citations2002Roberto Bagnara, Elisa Ricci +2 more
The Parma Polyhedra Library is presented, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings.
A technique for summarizing data access and its use in parallelism enhancing transformations
129 Citations1989Vasanth Balasundaram, Ken Kennedy
A technique for summarizing the data accesses in a given region is presented and it is shown how this summary can be used to detect and enhance task parallelism in a program.
The Octagon Abstract Domain
129 Citations2001Antoine Mid
OpenGrey (Institut de l'Information Scientifique et Technique)Weakly relational numerical abstract domains
128 Citations2004Antoine Miné, COUSOT, Patrick
The analysis framework presented in this thesis has been integrated within Astree, an analyzer for critical embedded software, and were instrumental in proving the absence of run-time errors in fly-by-wire softwares.
ACM Transactions on Programming Languages and SystemsModel-checking concurrent systems with unbounded integer variables
123 Citations1999Tevfik Bultan, R. Gerber +1 more
This article presents a new symbolic model checker which conservatively evaluates safety and liveness properties on programs with unbounded integer variables, using Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations.
Precise and efficient static array bound checking for large embedded C programs
121 Citations2004Arnaud Venet, Guillaume Brat
The design and implementation of a static array-bound checker for a family of embedded programs: the flight control software of recent Mars missions, which is the first distributed implementation of static analysis algorithms.
A Note on Chernikova's algorithm
120 Citations1992Hervé Le Verge
An implementation of Chernikova's algorithm for finding an irredundant set of vertices for a given polyhedron defined by a set of linear inequalities and equations based on the polyhedral cone duality principle is described.
Lecture notes in computer scienceConstraint-Based Linear-Relations Analysis
117 Citations2004Sriram Sankaranarayanan, Henny B. Sipma +1 more
By some efficient simplifications and approximations to the quantifier elimination procedure, not only does the method scale to higher dimensions, but also enjoys performance advantages for some larger examples.
Lecture notes in computer scienceNumeric Domains with Summarized Dimensions
90 Citations2004Denis Gopan, Frank DiMaio +3 more
This work introduces a systematic approach to designing summarizing abstract numeric domains from existing numeric domains that are of benefit to analyses that verify properties of systems with an unbounded number of numeric objects, such as shape analysis.
Verifying analog oscillator circuits using forward/backward abstraction refinement
82 Citations2006Goran Frehse, Bruce H. Krogh +1 more
A novel approach combining forward- and backward-reachability while iteratively refining partitions at each step is proposed, which can yield dramatic memory and runtime reductions.
USSR Computational Mathematics and Mathematical PhysicsAlgorithm for discovering the set of all the solutions of a linear programming problem
75 Citations1968N.V. Chernikoba
Science of Computer ProgrammingPrecise widening operators for convex polyhedra
67 Citations2005Roberto Bagnara, Patricia M. Hill +2 more
A framework for the systematic definition of new widening operators that are never less precise than a given widening is presented and an improvement to the well-known widening delay technique is suggested that allows one to gain precision while preserving its overall simplicity.
International Journal on Software Tools for Technology TransferWidening operators for powerset domains
66 Citations2007Roberto Bagnara, Patricia M. Hill +1 more
This paper defines three generic widening methodologies for the finite powerset abstract domain and is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully.
Lecture notes in computer scienceAutomatic Removal of Array Memory Leaks in Java
64 Citations2000Ran Shaham, Elliot K. Kolodner +1 more
A practical algorithm for statically detecting memory leaks occurring in arrays of objects in a garbage collected environment that is conservative, i.e., it never detects a leak on a piece of memory that is subsequently used by the program, although it may fail to identify some leaks.
HAL (Le Centre pour la Communication Scientifique Directe)Détermination automatique de relations linéaires vérifiées par les variables d'un programme
61 Citations1979Nicolas Halbwachs
Systeme d'equations en avant associe a un programme, definitions and resultats fondamentaux sur les polyedres convexes, applications de la methode, anders avec des travaux voisins.
The ASTR ´ EE Analyzer
61 Citations2005Patrick Cousot, Radhia Cousot +3 more
ASTR´ EE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language.
Lecture notes in computer scienceThe MathSAT 3 System
59 Citations2005Marco Bozzano, Roberto Bruttomesso +5 more
Satisfiability Modulo Theories can be seen as an extended form of propositional satisfiability, where propositions are either simple boolean propositions or quantifier-free atomic constraints in a specific theory.
Lecture notes in computer scienceA note on abstract interpretation strategies for hybrid automata
58 Citations1995Thomas A. Henzinger, Pei-Hsin Ho
Several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems are reported on.
Lecture notes in computer scienceAutomatic Rectangular Refinement of Affine Hybrid Systems
46 Citations2005Laurent Doyen, Thomas A. Henzinger +1 more
This method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton, and proves an optimality criterion for successive refinements.
Lecture notes in computer scienceEfficient Strongly Relational Polyhedral Analysis
46 Citations2005Sriram Sankaranarayanan, Michael A. Colón +2 more
This work proposes a polynomial time approach to strongly relational analysis of polyhedra analysis, and provides efficient implementations of join and post condition operations, achieving a trade off between performance and accuracy.
Lecture notes in computer scienceReachability Analysis of (Timed) Petri Nets Using Real Arithmetic
46 Citations1999Béatrice Bérard, Laurent Fribourg
It is shown that exact reachability analysis can be achieved by treating Petri nets integer variables (counters) as real-valued variables, and using Fourier-Motzkin procedure instead of Presburger elimination procedure, and can be safely analysed with performant tools, e.g. HyTech.
Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228)Some lessons from the HYTECH experience
44 Citations2003Thomas A. Henzinger, Jörg Preußig +1 more
An overview of the current status of HYTECH, some recent experiences analyzing three hybrid systems, and some desiderata for verification tools for hybrid systems are described.
Lecture notes in computer scienceGeneration of Basic Semi-algebraic Invariants Using Convex Polyhedra
42 Citations2005Roberto Bagnara, Enric Rodríguez-Carbonell +1 more
A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework based on overapproximating basic semi-algebraic sets, i.e., sets defined by conjunctions of polynometric inequalities by means of convex polyhedra.
2004 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No.04CH37601)Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction
40 Citations2004Goran Frehse, Zhi Han +1 more
This work proposes a novel assume-guarantee rule for hybrid systems based on simulation relations that makes it possible to perform compositional reasoning that is conservative in the sense of over-approximating the composed behaviors.
Formal Aspects of ComputingNot necessarily closed convex polyhedra and the double description method
40 Citations2005Roberto Bagnara, Patricia M. Hill +1 more
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.
Electronic Notes in Theoretical Computer ScienceTime Domain Verification of Oscillator Circuit Properties
35 Citations2006Goran Frehse, Bruce H. Krogh +2 more
Generic monitor automata are proposed to facilitate the application of hybrid system reachability computations to characterize time domain features of oscillatory behavior, such as bounds on the signal amplitude and jitter.
Theoretical Computer ScienceApplications of polyhedral computations to the analysis and verification of hardware and software systems
34 Citations2009Roberto Bagnara, Patricia M. Hill +1 more
The range of applications of polyhedral computations in this area is surveyed; an overview of the different classes of polyhedra that may be adopted; the main polyhedral operations required by automatic analyzers and verifiers are outlined; and some possible combinations ofpolyhedra with other numerical abstractions that have the potential to improve the precision of the analysis are looked at.
International Journal on Software Tools for Technology TransferWidening operators for powerset domains
31 Citations2006Roberto Bagnara, Patricia M. Hill +1 more
This paper defines three generic widening methodologies for the finite powerset abstract domain and is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully.
Lecture notes in computer scienceWidening Operators for Weakly-Relational Numeric Abstractions
30 Citations2005Roberto Bagnara, Patricia M. Hill +2 more
The construction of proper widening operators on several weakly-relational numeric abstractions are discussed, which actually consider the semantic abstract domains, whose elements are geometric shapes, instead of the syntactic abstract domains of constraint networks and matrices.
Theory and Practice of Logic ProgrammingcTI: a constraint-based termination inference tool for ISO-Prolog
29 Citations2005Fred Mesnard, Roberto Bagnara
ACM SIGPLAN NoticesA technique for summarizing data access and its use in parallelism enhancing transformations
28 Citations1989Vasanth Balasundaram, Ken Kennedy
Lecture notes in computer scienceGrids: A Domain for Analyzing the Distribution of Numerical Values
28 Citations2007Roberto Bagnara, K. Dobson +3 more
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 and shows how it exploit well-known techniques from linear algebra as well as a dual representation that allows for a concise and efficient implementation.
Optimization methods & softwareComputational experience with the reverse search vertex enumeration algorithm
27 Citations1998David Avis
Science of Computer ProgrammingA hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
24 Citations1998Roberto Bagnara
This work presents a class of constraint systems which allows for a smooth integration within an appropriate framework for the definition of non-standard semantics of constraint logic-based languages and proposes a general methodology for domain combination with asynchronous interaction.
Lecture notes in computer scienceStatic analyses of congruence properties on rational numbers (extended abstract)
19 Citations1997Philippe Granger
Several new static analysis frameworks applying to rational numbers are presented, designed for discovering congruence properties satisfied by rational variables of programs and exemplify the interest of all these analyses for optimizing the representation of rational or real valued variables.
Parallel Processing LettersOn Manipulating Z-Polyhedra Using a Canonical Representation
16 Citations1997Patrice Quinton, Sanjay Rajopadhye +1 more
A canonical representation for Z- Polyhedra is introduced which allows one to perform comparisons and transformations of Z-polyhedra with the help of a computational kernel on polyhedra.
Lecture notes in computer scienceVerifying Generalized Soundness of Workflow Nets
16 Citations2007Kees van Hee, Olivia Oanea +2 more
USSR Computational Mathematics and Mathematical PhysicsNumerical solution of a problem of optimum control of a nuclear reactor
14 Citations1965M.P. Leonchuk, А. С. Трофимов +1 more
Electronic Notes in Theoretical Computer ScienceSPHIN: A model checker for reconfigurable hybrid systems based on SPIN
12 Citations2006Hosung Song, Kevin J. Compton +1 more
SPHIN, a model checker for reconfigurable hybrid systems based on the modelChecker SPIN, is presented, observing that physical (analog) mobility can be modeled in the same way as logical (discrete) mobility is modeling in the @p-calculus by means of channel name passing.
Generation automatique de codes de transfert pour multiprocesseurs a memoires locales
12 Citations1991Martine Ancourt
Lecture notes in computer scienceFixed Point Iteration for Computing the Time Elapse Operator
11 Citations2006Sriram Sankaranarayanan, Henny B. Sipma +1 more
A time elapse operator is design that computes a symbolic over-approximation of time solutions to a continuous system starting from a given initial region and the performance of the technique is demonstrated on benchmark examples.
International Conference on Parallel Architectures and Compilation TechniquesThe modulo interval: a simple and practical representation for program analysis
10 Citations1999Tsuneo Nakanishi, Kensuke Fukuda +2 more
Compositional verification of hybrid systems with discrete interaction using simulation relations
8 Citations2005Goran Frehse
It is shown that for hybrid systems without shared variables, which therefore only interact at discrete events, this simulation preorder is compositional, and assume-guarantee rules that help to counter the state explosion problem are presented.
Lecture notes in computer sciencePolyhedra-Based Approach for Incremental Validation of Real-Time Systems
6 Citations2005David Doose, Zoubir Mammeri
This method is able to model and validate all the classical features of real-time systems, without any pessimism, while guaranteeing the terminaison of the validation process.
Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis
5 Citations2004Ron Ellenbogen
This work presents a interprocedural C String Static Verifier (iCSSV), a whole program analysis algorithm for verifying the safety of string operations in C programs that automatically proves linear relationships among pointer expressions.
Lecture notes in computer scienceStatic Analysis of Gated Data Dependence Graphs
3 Citations2004Charles Hymans, Eben Upton
This paper presents the first example of a static analysis of the gated data dependence graph developed using the methodology of abstract interpretation, and is shown to be sound with respect to a concrete semantics for the representation.
…