A bibliography of papers that were consulted and/or written for the design and implementation of the Parma Polyhedra Library. Copyright (C) 2001-2010 Roberto Bagnara Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com) This BibTeX database is made available under the Open Data Commons Attribution License (ODC-By) v1.0, which is reproduced below for your convenience and available at http://opendatacommons.org/licenses/by/1.0/ Summarizing: - You are free: to copy, distribute and use the database; to produce works from the database; to modify, transform and build upon the database. - You must attribute any public use of the database, or works produced from the database, in the manner specified in the license. For any use or redistribution of the database, or works produced from it, you must make clear to others the license of the database and keep intact any notices on the original database. @PREAMBLE{ "\newcommand{\noopsort}[1]{}" } @PhdThesis{Ancourt91th, Author = "C. Ancourt", Title = "G\'en\'eration automatique de codes de transfert pour multiprocesseurs \`a m\'emoires locales", School = "Universit\'e de Paris VI", Address = "Paris, France", Month = mar, Year = 1991, Abstract = "Parallel tasks generated by automatic parallelizers do not take advantage of supercomputer memory hierarchies. This thesis presents algorithms to transform a parallel task into an equivalent one that uses data with fast access memory. Algorithms to automatically generate code to move data between two different memory levels of (super)computer are presented. These copy codes should move back and forth array elements that are accessed when an elementary processor execute an array reference located in a set of loops. This set of array elements is characterized by a set of integer points in $\mathcal{Z}^p$ that is not necessarily a convex polyhedron. In the case of data transfers from global memory to local memory, it is possible to copy a superset of accessed elements, for instance its convex hull. A trade-off has to be made between local memory space, transfer volume and loop bound complexity. To copy data back from local memory to global memory is more difficult because global memory consistency must be preserved. Each processor (or processus) should only copy its own results to avoid errors and, secondarily, to decrease global memory traffic. The input of our main algorithm is an integer convex polyhedron defining the computation space and an affine function representing the index expressions. Its output is set of nested loops containing a new array reference whose execution copies exactly accessed elements. Each element is copied only once. Loop bound expressions use integer divisions to generate non-convex sets. For most practical programs this algorithm provides optimal code in number of data movements and control overhead. Associated with a dependence analysis phase, it can be used to generate data movements in distributed memory multiprocessors. When data partitionning in local memories is specified, it eliminates most of execution guards used to compute only local values on each processor." } @PhdThesis{Bagnara97th, Author = "R. Bagnara", Title = "Data-Flow Analysis for Constraint Logic-Based Languages", School = "Dipartimento di Informatica, Universit\`a di Pisa", Address = "Pisa, Italy", Month = mar, Year = 1997, Note = "Printed as Report TD-1/97", Abstract = "We aim at the the development of precise, practical, and theoretically well-founded data-flow analyzers for constraint logic-based languages. The design and development of such an analyzer fostered a number of research problems that we had to address. A hierarchy of constraint systems is introduced that is suitable for designing and combining abstract domains. The rational construction of a generic domain for the structural analysis of CLP programs is presented. We also address the problem of the ``missing \emph{occur-check}'' in many implemented languages. We introduce a new family of domains, based on constraint propagation techniques, for the abstraction of the numerical leaves that occur in the terms of CLP languages. Despite the fact that groundness analysis for logic-based languages is a widely studied subject, a novel domain for groundness analysis is presented that outperforms the existing domains from several points of view. Finally, we present a bottom-up analysis technique for CLP languages that allows for the precise derivation of both call- and success-patterns preserving the connection between them." } @Article{Bagnara98SCP, Author = "R. Bagnara", Title = "A Hierarchy of Constraint Systems for Data-Flow Analysis of Constraint Logic-Based Languages", Journal = "Science of Computer Programming", Volume = 30, Number = "1--2", Publisher = "Elsevier", Year = 1998, Pages = "119--155", Abstract = "Many interesting analyses for constraint logic-based languages are aimed at the detection of \emph{monotonic} properties, that is to say, properties that are preserved as the computation progresses. Our basic claim is that most, if not all, of these analyses can be described within a unified notion of constraint domains. We present a class of constraint systems that allows for a smooth integration within an appropriate framework for the definition of non-standard semantics of constraint logic-based languages. Such a framework is also presented and motivated. We then show how such domains can be built, as well as construction techniques that induce a hierarchy of domains with interesting properties. In particular, we propose a general methodology for domain combination with asynchronous interaction (i.e., the interaction is not necessarily synchronized with the domains' operations). By following this methodology, interesting combinations of domains can be expressed with all the the semantic elegance of concurrent constraint programming languages.", URL = "http://bugseng.com/products/ppl/documentation/Bagnara98SCP.pdf" } @Techreport{BagnaraDHMZ05TR, Author = "R. Bagnara and K. Dobson and P. M. Hill and M. Mundell and E. Zaffanella", Title = "A Linear Domain for Analyzing the Distribution of Numerical Values", Number = "2005.06", Type = "Report", Institution = "School of Computing, University of Leeds, UK", Year = 2005, Abstract = "This paper explores the abstract domain of \emph{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. Besides the bare abstract domain, we present a complete set of operations on grids that includes all that is necessary to define the abstract semantics and the widening operators required to compute it in a finite number of steps. 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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraDHMZ05TR.pdf", } @InProceedings{BagnaraDHMZ07, Author = "R. Bagnara and K. Dobson and P. M. Hill and M. Mundell and E. Zaffanella", Title = "Grids: A Domain for Analyzing the Distribution of Numerical Values", Booktitle = "Logic-based Program Synthesis and Transformation, 16th International Symposium", Address = "Venice, Italy", Editor = "G. Puebla", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 4407, ISBN = "3-540-71409-X", Year = 2007, Pages = "219--235", Abstract = "This paper explores the abstract domain of \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraDHMZ07.pdf" } @Misc{BagnaraDHMZ06b, Author = "R. Bagnara and K. Dobson and P. M. Hill and M. Mundell and E. Zaffanella", Title = "A Practical Tool for Analyzing the Distribution of Numerical Values", Year = 2006, Note = "Available at \url{http://www.comp.leeds.ac.uk/hill/Papers/papers.html}.", Abstract = "The abstract domain of grids (or lattices) is 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 that program variables can take. This paper explores how this domain may be used in program analysis, describing grid operations such as affine image, affine preimage and widenings needed by such an application. The paper also shows how any grid may be approximated by a less precise non-relational grid and describes how such an approximation can be computed. Illustrative examples show how the domain may be used in the analysis of programs containing simple assignment statements, while loops and recursive procedures." } @Misc{BagnaraHMZ04EA, Author = "R. Bagnara and P. M. Hill and E. Mazzi and E. Zaffanella", Title = "Widening Operators for Weakly-Relational Numeric Abstractions", Howpublished = "Report {\tt arXiv:cs.PL/0412043}", Year = 2004, Note = "Extended abstract. Contribution to the \emph{International workshop on ``Numerical \& Symbolic Abstract Domains''} (NSAD'05, Paris, January 21, 2005). Available at \url{http://arxiv.org/} and \url{http://bugseng.com/products/ppl/}", Abstract = "We discuss the divergence problems recently identified in some extrapolation operators for weakly-relational numeric domains. We identify the cause of the divergences and point out that resorting to more concrete, syntactic domains can be avoided by researching suitable algorithms for the elimination of redundant constraints in the chosen representation.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHMZ04EA.pdf" } @InProceedings{BagnaraHZ02a, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "A New Encoding of Not Necessarily Closed Convex Polyhedra", Booktitle = "Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems", Address = "Madrid, Spain", Editor = "M. Carro and C. Vacheret and K.-K. Lau", Year = 2002, Pages = "147--153", Note = "Published as TR Number CLIP4/02.0, Universidad Polit\'ecnica de Madrid, Facultad de Inform\'atica", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ02a.pdf" } @TechReport{BagnaraHZ02TR, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "A New Encoding and Implementation of Not Necessarily Closed Convex Polyhedra", Number = 305, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2002, Note = "Available at \url{http://www.cs.unipr.it/Publications/}", Abstract = "Convex polyhedra, commonly employed for the analysis and verification of both hardware and software, may be defined either by a finite set of linear inequality constraints or by finite sets of generating points and rays of the polyhedron. 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 vector space having one extra dimension and reuse the tools and techniques already available for closed polyhedra. Previously, this embedding has been designed so that a constant number of constraints and a linear number of generators have to be added to the original NNC specification of the polyhedron. In this paper we explore an alternative approach: while still using an extra dimension to represent the NNC polyhedron by a closed polyhedron, the new embedding adds a linear number of constraints and a constant number of generators. We discuss the relative benefits of these two implementations and how the choice of representation can affect the efficiency of the polyhedral operations. As far as the issue of providing a non-redundant description of the NNC polyhedron is concerned, we generalize the results established in a previous paper so that they apply to both encodings." } @Article{BagnaraHRZ05SCP, Author = "R. Bagnara and P. M. Hill and E. Ricci and E. Zaffanella", Title = "Precise Widening Operators for Convex Polyhedra", Journal = "Science of Computer Programming", Volume = 58, Number = "1--2", Publisher = "Elsevier", Year = 2005, Pages = "28--56", Abstract = "In the context of static analysis via abstract interpretation, convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of \emph{standard widening} since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it. We present a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new widening operator that improves on the standard widening by combining several heuristics. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows to gain precision while preserving its overall simplicity.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHRZ05SCP.pdf" } @TechReport{BagnaraHMZ05TR, Author = "R. Bagnara and P. M. Hill and E. Mazzi and E. Zaffanella", Title = "Widening Operators for Weakly-Relational Numeric Abstractions", Number = 399, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2005, Note = "Available at \url{http://www.cs.unipr.it/Publications/}", Abstract = "We discuss the construction of proper widening operators on several weakly-relational numeric abstractions. Our proposal differs from previous ones in that we actually consider the semantic abstract domains, whose elements are \emph{geometric shapes}, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices. Since the closure by entailment operator preserves geometric shapes, but not their syntactic expressions, our widenings are immune from the divergence issues that could be faced by the previous approaches when interleaving the applications of widening and closure. The new widenings, which are variations of the \emph{standard widening} for convex polyhedra defined by Cousot and Halbwachs, can be made as precise as the previous proposals working on the syntactic domains. The implementation of each new widening relies on the availability of an effective reduction procedure for the considered constraint description: we provide such an algorithm for the domain of \emph{octagonal shapes}.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHMZ05TR.pdf" } @InProceedings{BagnaraHMZ05, Author = "R. Bagnara and P. M. Hill and E. Mazzi and E. Zaffanella", Title = "Widening Operators for Weakly-Relational Numeric Abstractions", Booktitle = "Static Analysis: Proceedings of the 12th International Symposium", Address = "London, UK", Editor = "C. Hankin and I. Siveroni", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 3672, ISBN = "3-540-28584-9", Year = 2005, Pages = "3--18", Abstract = "We discuss the construction of proper widening operators on several weakly-relational numeric abstractions. Our proposal differs from previous ones in that we actually consider the semantic abstract domains, whose elements are \emph{geometric shapes}, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices. Since the closure by entailment operator preserves geometric shapes, but not their syntactic expressions, our widenings are immune from the divergence issues that could be faced by the previous approaches when interleaving the applications of widening and closure. The new widenings, which are variations of the \emph{standard widening} for convex polyhedra defined by Cousot and Halbwachs, can be made as precise as the previous proposals working on the syntactic domains. The implementation of each new widening relies on the availability of an effective reduction procedure for the considered constraint description: we provide such an algorithm for the domain of \emph{octagonal shapes}.", } @Techreport{BagnaraMPZ10TR, Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella", Title = "The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version", Number = 498, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2010, Note = "Superseded by \cite{BagnaraMPZ12TR}.", Abstract = "The classical technique for proving termination of a generic sequential computer program involves the synthesis of a \emph{ranking function} for each loop of the program. \emph{Linear} ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van~Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers." } @Misc{BagnaraMPZ12TR, Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella", Title = "The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version", Howpublished = "Report {\tt arXiv:cs.PL/1004.0944v2}", Year = 2012, Note = "Available at \url{http://arxiv.org/} and \url{http://bugseng.com/products/ppl/}. Improved version of \cite{BagnaraMPZ10TR}.", Abstract = "The classical technique for proving termination of a generic sequential computer program involves the synthesis of a \emph{ranking function} for each loop of the program. \emph{Linear} ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van~Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers." } @Article{BagnaraMPZ12IC, Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella", Title = "A New Look at the Automatic Synthesis of Linear Ranking Functions", Journal = "Information and Computation", Publisher = "Elsevier Science B.V.", Year = 2012, Note = "To appear.", Abstract = "The classical technique for proving termination of a generic sequential computer program involves the synthesis of a \emph{ranking function} for each loop of the program. \emph{Linear} ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van~Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers." } @InProceedings{BagnaraRZH02, Author = "R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill", Title = "Possibly Not Closed Convex Polyhedra and the {Parma Polyhedra Library}", Booktitle = "Static Analysis: Proceedings of the 9th International Symposium", Address = "Madrid, Spain", Editor = "M. V. Hermenegildo and G. Puebla", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2477, ISBN = "3-540-44235-9", Pages = "213--229", Year = 2002, Abstract = "The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P.~Cousot and N.~Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. Furthermore, there is inadequate support for polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraRZH02.pdf" } @TechReport{BagnaraRZH02TR, Author = "R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill", Title = "Possibly Not Closed Convex Polyhedra and the {Parma Polyhedra Library}", Number = 286, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = "{\noopsort{a}}2002", Note = "See also \cite{BagnaraRZH02TRerrata}. Available at \url{http://www.cs.unipr.it/Publications/}", Abstract = "The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P.~Cousot and N.~Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. These limitations concern inaccuracies in the documentation of the underlying theory, code and interfaces; numeric overflow and underflow; use of not fully dynamic data-structures and poor mechanisms for error handling and recovery. In addition, there is inadequate support for polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings." } @Misc{BagnaraRZH02TRerrata, Author = "R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill", Title = "Errata for Technical Report {``Quaderno 286''}", Howpublished = "Available at \url{http://www.cs.unipr.it/Publications/}", Year = "{\noopsort{b}}2002", Note = "See \cite{BagnaraRZH02TR}" } @InProceedings{BagnaraHRZ03, Author = "R. Bagnara and P. M. Hill and E. Ricci and E. Zaffanella", Title = "Precise Widening Operators for Convex Polyhedra", Booktitle = "Static Analysis: Proceedings of the 10th International Symposium", Address = "San Diego, California, USA", Editor = "R. Cousot", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2694, Year = 2003, Pages = "337--354", Abstract = "Convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating convergence of the fixpoint computation. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of \emph{standard widening} since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it. We present a framework for the systematic definition of new and precise widening operators for convex polyhedra. The framework is then instantiated so as to obtain a new widening operator that combines several heuristics and uses the standard widening as a last resort so that it is never less precise. A preliminary experimental evaluation has yielded promising results.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHRZ03.pdf" } @TechReport{BagnaraHRZ03TR, Author = "R. Bagnara and P. M. Hill and E. Ricci and E. Zaffanella", Title = "Precise Widening Operators for Convex Polyhedra", Number = 312, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2003, Note = "Available at \url{http://www.cs.unipr.it/Publications/}", Abstract = "Convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating convergence of the fixpoint computation. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of \emph{standard widening} since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is demand for more precise widening operators that still has not been fulfilled. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it. We present a framework for the systematic definition of new and precise widening operators for convex polyhedra. The framework is then instantiated so as to obtain a new widening operator that combines several heuristics and uses the standard widening as a last resort so that it is never less precise. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows to gain precision while preserving its overall simplicity." } @InProceedings{BagnaraHZ03a, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "A New Encoding and Implementation of Not Necessarily Closed Convex Polyhedra", Booktitle = "Proceedings of the 3rd Workshop on Automated Verification of Critical Systems", Address = "Southampton, UK", Editor = "M. Leuschel and S. Gruner and S. {Lo Presti}", Year = 2003, Pages = "161--176", Note = "Published as TR Number DSSE-TR-2003-2, University of Southampton", Abstract = "Convex polyhedra, commonly employed for the analysis and verification of both hardware and software, may be defined either by a finite set of linear inequality constraints or by finite sets of generating points and rays of the polyhedron. 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 vector space having one extra dimension and reuse the tools and techniques already available for closed polyhedra. Previously, this embedding has been designed so that a constant number of constraints and a linear number of generators have to be added to the original NNC specification of the polyhedron. In this paper we explore an alternative approach: while still using an extra dimension to represent the NNC polyhedron by a closed polyhedron, the new embedding adds a linear number of constraints and a constant number of generators. We discuss the relative benefits of these two implementations and how the choice of representation can affect the efficiency of the polyhedral operations. As far as the issue of providing a non-redundant description of the NNC polyhedron is concerned, we generalize the results established in a previous paper so that they apply to both encodings.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ03a.pdf" } @InProceedings{BagnaraHZ03b, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Widening Operators for Powerset Domains", Booktitle = "Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference (VMCAI 2004)", Address = "Venice, Italy", Editor = "B. Steffen and G. Levi", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2937, ISBN = "3-540-20803-8", Year = 2003, Pages = "135--148", Abstract = "The \emph{finite powerset construction} upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define two generic widening operators for the finite powerset abstract domain. Both 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. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ03b.pdf" } @TechReport{BagnaraHZ04TR, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Widening Operators for Powerset Domains", Number = 349, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2004, Note = "Available at \url{http://www.cs.unipr.it/Publications/}", Abstract = "The \emph{finite powerset construction} upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define two generic widening operators for the finite powerset abstract domain. Both 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. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.", } @Article{BagnaraHZ05FAC, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Not Necessarily Closed Convex Polyhedra and the Double Description Method", Journal = "Formal Aspects of Computing", Publisher = "Springer-Verlag, London", Volume = "17", Number = "2", Pages = "222--257", Year = 2005, ISSN = "0934-5043", 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 \emph{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.", } @Article{BagnaraHZ06STTT, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Widening Operators for Powerset Domains", Journal = "Software Tools for Technology Transfer", Publisher = "Springer-Verlag, Berlin", Volume = 8, Number = "4/5", Pages = "449--466", Year = 2006, Note = "In the printed version of this article, all the figures have been improperly printed (rendering them useless). See \cite{BagnaraHZ06STTTerratum}.", Abstract = "The \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ06STTT.pdf" } @Article{BagnaraHZ06STTTerratum, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Widening Operators for Powerset Domains", Journal = "Software Tools for Technology Transfer", Publisher = "Springer-Verlag, Berlin", Volume = 9, Number = "3/4", Pages = "413--414", Year = 2007, Note = "Erratum to \cite{BagnaraHZ06STTT} containing all the figures properly printed." } @TechReport{BagnaraHZ06TR, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems", Number = 457, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2006, Note = "Available at \url{http://www.cs.unipr.it/Publications/}. Also published as {\tt arXiv:cs.MS/0612085}, available from \url{http://arxiv.org/}.", Abstract = "Since its inception as a student project in 2001, initially just for the handling (as the name implies) of convex polyhedra, the \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ06TR.pdf" } @TechReport{BagnaraHZ07TRa, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems", Number = 458, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2007, Note = "Available at \url{http://www.cs.unipr.it/Publications/}. Also published as {\tt arXiv:cs.CG/0701122}, available from \url{http://arxiv.org/}.", Abstract = "Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such applications, the identification of an appropriate complexity-precision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ07TRa.pdf" } @TechReport{BagnaraHZ07TRb, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "An Improved Tight Closure Algorithm for Integer Octagonal Constraints", Number = 467, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2007, Note = "Available at \url{http://www.cs.unipr.it/Publications/}. Also published as {\tt arXiv:0705.4618v2 [cs.DS]}, available from \url{http://arxiv.org/}.", Abstract = "Integer octagonal constraints (a.k.a.\ \emph{Unit Two Variables Per Inequality} or \emph{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 \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ07TRb.pdf" } @Inproceedings{BagnaraHZ08, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "An Improved Tight Closure Algorithm for Integer Octagonal Constraints", Booktitle = "Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008)", Address = "San Francisco, USA", Editor = "F. Logozzo and D. Peled and L. Zuck", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 4905, ISBN = "3-540-78162-2", Year = 2008, Pages = "8--21", Abstract = "Integer octagonal constraints(a.k.a.\ \emph{Unit Two Variables Per Inequality} or \emph{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 \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ08.pdf" } @Article{BagnaraHZ08SCP, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems", Journal = "Science of Computer Programming", Volume = 72, Number = "1--2", Pages = "3--21", Publisher = "Elsevier", Year = 2008, Abstract = "Since its inception as a student project in 2001, initially just for the handling (as the name implies) of convex polyhedra, the \emph{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.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ08SCP.pdf" } @Article{BagnaraHZ10CGTA, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions", Journal = "Computational Geometry: Theory and Applications", Volume = 43, Number = 5, Pages = "453--473", Publisher = "Elsevier", Year = 2010, Abstract = "Deciding whether the union of two convex polyhedra is itself a convex polyhedron is a basic problem in polyhedral computations; having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In such application fields though, general convex polyhedra are just one among many, so-called, \emph{numerical abstractions}, which range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices ---that is, partial orders where any finite set of elements has a least upper bound---, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra ---which, as far as we know, is the only one already studied in the literature--- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ10CGTA.pdf" } @Article{BagnaraHZ09TCS, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems", Journal = "Theoretical Computer Science", Volume = 410, Number = 46, Pages = "4672--4691", Publisher = "Elsevier", Year = 2009, Abstract = "Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such applications, the identification of an appropriate complexity-precision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ09TCS.pdf" } @Article{BagnaraHZ09FMSD, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness", Journal = "Formal Methods in System Design", Volume = 35, Number = 3, Publisher = "Springer-Verlag, Berlin", Year = 2009, Pages = "279--323", Abstract = "Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal analysis and verification of software and hardware systems. We address the problems to be solved for the construction of full-fledged, efficient and provably correct abstract domains based on such constraints. We first propose to work with \emph{semantic} abstract domains, whose elements are \emph{geometric shapes}, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices on which the previous proposals are based. This allows to solve, once and for all, the problem whereby \emph{closure by entailment}, a crucial operation for the realization of such domains, seemed to impede the realization of proper widening operators. In our approach, the implementation of widenings relies on the availability of an effective reduction procedure for the considered constraint description: one for the domain of \emph{bounded difference shapes} already exists in the literature; we provide algorithms for the significantly more complex cases of rational and integer \emph{octagonal shapes}. We also improve upon the state-of-the-art by presenting, along with their proof of correctness, closure by entailment algorithms of reduced complexity for domains based on rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ09FMSD.pdf" } @Techreport{BagnaraHZ09TRa, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions", Number = 492, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2009, Note = "Available at \url{http://www.cs.unipr.it/Publications/}. A corrected and improved version (corrected an error in the statement of condition (3) of Theorem~3.6, typos corrected in statement and proof of Theorem~6.8) has been published in \cite{BagnaraHZ09TRb}.", Abstract = "Deciding whether the union of two convex polyhedra is a convex polyhedron is a basic problem in polyhedral computation having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In these application fields, though, general convex polyhedra are only one among many so-called \emph{numerical abstractions}: these range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices ---that is, partial orders where any finite set of elements has a least upper bound---, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra ---which, as far as we know, is the only one already studied in the literature--- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ09TRa.pdf" } @Misc{BagnaraHZ09TRb, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions", Howpublished = "Report {\tt arXiv:cs.CG/0904.1783}", Year = 2009, Note = "Available at \url{http://arxiv.org/} and \url{http://bugseng.com/products/ppl/}", Abstract = "Deciding whether the union of two convex polyhedra is itself a convex polyhedron is a basic problem in polyhedral computations; having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In such application fields though, general convex polyhedra are just one among many, so-called, \emph{numerical abstractions}, which range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices ---that is, partial orders where any finite set of elements has a least upper bound---, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra ---which, as far as we know, is the only one already studied in the literature--- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.", URL = "http://bugseng.com/products/ppl/documentation/BagnaraHZ09TRb.pdf" } @InProceedings{BalasundaramK89, Author = "V. Balasundaram and K. Kennedy", Title = "A Technique for Summarizing Data Access and Its Use in Parallelism Enhancing Transformations", Booktitle = "Proceedings of the ACM SIGPLAN'89 Conference on Programming Language Design and Implementation (PLDI)", Address = "Portland, Oregon, USA", Editor = "B. Knobe", Series = "ACM SIGPLAN Notices", Volume = "24(7)", Publisher = "ACM Press", Year = 1989, Pages = "41--53", } @Techreport{BemporadFT00TR, Author = "A. Bemporad and K. Fukuda and F. D. Torrisi", Title = "Convexity Recognition of the Union of Polyhedra", Number = "AUT00-13", Type = "Report", Institution = "Automatic Control Laboratory, ETHZ", Address = "Zurich, Switzerland", Year = 2000, Abstract = "In this paper we consider the following basic problem in polyhedral computation: Given two polyhedra in $R^d$, $P$ and $Q$, decide whether their union is convex, and, if so, compute it. We consider the three natural specializations of the problem: (1) when the polyhedra are given by half-spaces (H-polyhedra) (2) when they are given by vertices and extreme rays (V-polyhedra) (3) when both H- and V-polyhedral representations are available. Both the bounded (polytopes) and the unbounded case are considered. We show that the first two problems are polynomially solvable, and that the third problem is strongly-polynomially solvable.", URL = "http://control.ee.ethz.ch/index.cgi?page=publications;action=details;id=62" } @Article{BemporadFT01, Author = "A. Bemporad and K. Fukuda and F. D. Torrisi", Title = "Convexity Recognition of the Union of Polyhedra", Journal = "Computational Geometry: Theory and Applications", Volume = 18, Number = 3, Publisher = "Elsevier", Year = 2001, ISSN = "0925-7721", Pages = "141--154", Abstract = "In this paper we consider the following basic problem in polyhedral computation: Given two polyhedra in $R^d$, $P$ and $Q$, decide whether their union is convex, and, if so, compute it. We consider the three natural specializations of the problem: (1) when the polyhedra are given by halfspaces (H-polyhedra), (2) when they are given by vertices and extreme rays (V-polyhedra), and (3) when both H- and V-polyhedral representations are available. Both the bounded (polytopes) and the unbounded case are considered. We show that the first two problems are polynomially solvable, and that the third problem is strongly-polynomially solvable.", } @InProceedings{BessonJT99, Author = "F. Besson and T. P. Jensen and J.-P. Talpin", Title = "Polyhedral Analysis for Synchronous Languages", Booktitle = "Static Analysis: Proceedings of the 6th International Symposium", Address = "Venice, Italy", Editor = "A. Cortesi and G. Fil\'e", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 1694, ISBN = "3-540-66459-9", Year = 1999, Pages = "51--68", Abstract = "We define an operational semantics for the \textsc{Signal} language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of a reactive system. A distinguished feature of the analysis is that it is expressed and proved correct with respect to the source program rather than on an intermediate representation of the program. The analysis calculates a safe approximation to the set of reachable states by a symbolic fixed point computation in the domain of convex polyhedra using a novel widening operator based on the convex hull representation of polyhedra." } @InProceedings{BjorndalenA05, Author = "J. M. Bj{\o}rndalen and O. Anshus", Title = "Lessons Learned in Benchmarking --- {Floating} Point Benchmarks: Can You Trust Them?", Booktitle = "Proceedings of the \emph{Norsk informatikkonferanse 2005} (NIK 2005)", Address = "Bergen, Norway", Publisher = "Tapir Akademisk Forlag", ISBN = "82-519-2081-7", Year = 2005, Pages = "89--100", Abstract = "Benchmarks are important tools for understanding the implication of design choices for systems, and for studying increasingly complex hardware architectures and software systems. One of the assumptions for benchmarking within systems research seems to be that the execution time of floating point operations do not change much with different input values. We report on a problem where a textbook benchmark showed significant variation in execution time depending on the input values, and how a small fraction of \emph{denormalized} floating point values (a representation automatically used by the CPU to represent values close to zero) in the benchmark could lead to the wrong conclusions about the relative efficiency of PowerPC and Intel P4 machines. Furthermore, a parallel version of the same benchmark is demonstrated to incorrectly indicate scalability problems in the application or communication subsystem. There is significant overhead in handling these exceptions on-chip on modern Intel hardware, even if the program can continue uninterrupted. We have observed that the execution time of benchmarks can increase by up to two orders of magnitude. In one benchmark, 3.88\% denormalized numbers in a matrix slowed down the benchmark by a factor 3.83. We suggest some remedies and guidelines for avoiding the problem.", URL = "http://www.cs.uit.no/~johnm/publications/pdf/bjorndalen2005lessons.pdf" } @InCollection{BlanchetCCFMMMR02, Author = "B. Blanchet and P. Cousot and R. Cousot and J. Feret and L. Mauborgne and A. Min\'e and D. Monniaux and X. Rival", Title = "Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software", Booktitle = "The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday]", Editor = "T. {\AE.} Mogensen and D. A. Schmidt and I. {Hal Sudborough}", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2566, ISBN = "3-540-00326-6", Year = 2002, Pages = "85--108", Abstract = "We report on a successful preliminary experience in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expansion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees." } @Article{BultanGP99, Author = "T. Bultan and R. Gerber and W. Pugh", Title = "Model-Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations, and Experimental Results", Journal = "ACM Transactions on Programming Languages and Systems", Volume = 21, Number = 4, Publisher = "ACM Press", Year = 1999, ISSN = "0164-0925", Pages = "747--789", Abstract = "Model checking is a powerful technique for analyzing large, finite-state systems. In an infinite state system, however, many basic properties are undecidable. In this article, we present a new symbolic model checker which conservatively evaluates safety and liveness properties on programs with unbounded integer variables. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems.", URL = "http://www.cs.ucsb.edu/~bultan/publications/toplas.ps" } @Article{Chernikova64, Author = "N. V. Chernikova", Title = "Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Equations", Journal = "U.S.S.R. Computational Mathematics and Mathematical Physics", Publisher = "MAIK NAUKA/Interperiodica Publishing, Moscow", Volume = 4, Number = 4, Pages = "151--158", Year = 1964 } @Article{Chernikova65, Author = "N. V. Chernikova", Title = "Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Inequalities", Journal = "U.S.S.R. Computational Mathematics and Mathematical Physics", Publisher = "MAIK NAUKA/Interperiodica Publishing, Moscow", Volume = 5, Number = 2, Pages = "228--233", Year = 1965, Abstract = "The present note proposes a computational scheme for finding a general formula for the non-negative solutions of a system of linear inequalities analogous to the scheme described in \cite{Chernikova64} for finding a general formula for the non-negative solutions of a system of linear equations." } @Article{Chernikova68, Author = "N. V. Chernikova", Title = "Algorithm for Discovering the Set of all Solutions of a Linear Programming Problem", Journal = "U.S.S.R. Computational Mathematics and Mathematical Physics", Publisher = "MAIK NAUKA/Interperiodica Publishing, Moscow", Volume = 8, Number = 6, Pages = "282--293", Year = 1968, Abstract = "In this paper two versions of a canonical algorithm for discovering all the optimal solutions of a linear programming problem with the condition of non-negativeness of the variables are presented: the first for the case of canonical notation, the second for the standard notation." } @InProceedings{CousotC76, Author = "P. Cousot and R. Cousot", Title = "Static Determination of Dynamic Properties of Programs", Booktitle = "Proceedings of the Second International Symposium on Programming", Editor = "B. Robinet", Address = "Paris, France", Publisher = "Dunod, Paris, France", Pages = "106--130", Year = 1976, Abstract = "In high level languages, compile time type verifications are usually incomplete, and dynamic coherence checks must be inserted in object code. For example, in PASCAL one must dynamically verify that the values assigned to subrange type variables, or index expressions lie between two bounds, or that pointers are not \texttt{nil}, ... We present here a general algorithm allowing most of these certifications to be done at compile time.", URL = "http://www.di.ens.fr/~cousot/publications.www/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf" } @InProceedings{CousotC79, Author = "P. Cousot and R. Cousot", Title = "Systematic Design of Program Analysis Frameworks", Booktitle = "Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages", Publisher = "ACM Press", Address = "San Antonio, TX, USA", Pages = "269--282", Year = 1979, Abstract = "Semantic analysis of programs is essential in optimizing compilers and program verification systems. It encompasses data flow analysis, data type determination, generation of approximate invariant assertions, etc. Several recent papers (among others Cousot \& Cousot[77a], Graham & Wegman[76], Kam & Ullmann[76], Killdall[73], Rosen[78], Tarjan[76], Wegbreit[75]) have introduced abstract approaches to program analysis which are tantamount to the use of a \emph{program analysis framework} $(A, t, \gamma)$ where $A$ is a lattice of (approximate) assertions, $t$ is an (approximate) predicate transformer and $\gamma$ is an often implicit function specifying the meaning of the elements of $A$. This paper is devoted to the systematic and correct design of program analysis frameworks with respect to a formal semantics.", URL = "http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-79-ACM-p269--282-1979.pdf" } @InProceedings{CousotC92-PLILP, Author = "P. Cousot and R. Cousot", Title = "Comparing the {Galois} Connection and Widening/Narrowing Approaches to Abstract Interpretation", Booktitle = "Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming", Address = "Leuven, Belgium", Editor = "M. Bruynooghe and M. Wirsing", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 631, ISBN = "3-540-55844-6", Pages = "269--295", Year = 1992, Abstract = "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 (or lattices satisfying the chain condition).", URL = "http://www.di.ens.fr/~cousot/publications.www/CousotCousot-PLILP-92-LNCS-n631-p269--295-1992.pdf" } @InProceedings{CousotH78, Author = "P. Cousot and N. Halbwachs", Title = "Automatic Discovery of Linear Restraints Among Variables of a Program", Booktitle = "Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages", Address = "Tucson, Arizona", Publisher = "ACM Press", Pages = "84--96", Year = 1978, Abstract = "The model of abstract interpretation of programs developed by Cousot & Cousot [1976] and Cousot & Cousot [1977] is applied to the static determination of linear equality or inequality relations among variables of programs.", URL = "http://www.di.ens.fr/~cousot/publications.www/CousotHalbwachs-POPL-78-ACM-p84--97-1978.pdf" } @Book{Dantzig63, Author = "G. B. Dantzig", Title = "Linear Programming and Extensions", Publisher = "Princeton University Press", Address = "Princeton, NJ", Year = 1963 } @Article{Feautrier88, Author = "P. Feautrier", Title = "Parametric Integer Programming", Journal = "RAIRO Recherche Op\'erationnelle", Year = 1988, Volume = 22, Number = 3, Pages = "243--268", Abstract = "When analysing computer programs (especially numerical programs in which arrays are used extensively), one is often confronted with integer programming problems. These problems have three peculiarities: feasible points are ranked according to lexicographic order rather than the usual linear economic function; the feasible set depends on integer parameters; one is interested only in exact solutions. The difficulty is somewhat alleviated by the fact that problems sizes are usually quite small. In this paper we show that: the classical simplex algorithm has no difficulty in handling lexicographic ordering; the algorithm may be executed in symbolic mode, thus giving the solution of continuous parametric problems; the method may be extended to problems in integers. We prove that the resulting algorithm always terminate and give an estimate of its complexity." } @Manual{FeautrierCB07, Author = "P. Feautrier and J.-F. Collard and C. Bastoul", Title = "{PIP/PipLib}: A Solver for Parametric Integer Programming Problems", Edition = "5.0", Note = "Distributed with {PIP/PipLib} 1.4.0", Month = jul, Year = 2007, Abstract = "This manual is for PIP and PipLib version 1.4.0, a software which solves Parametric Integer Programming problems. That is, PIP finds the lexicographic minimum of the set of integer points which lie inside a convex polyhedron, when that polyhedron depends linearly on one or more integral parameters." } @Misc{Fukuda98, Author = "K. Fukuda", Title = "Polyhedral Computation {FAQ}", Howpublished = "Swiss Federal Institute of Technology, Lausanne and Zurich, Switzerland, available at \url{http://www.ifor.math.ethz.ch/~fukuda/polyfaq/polyfaq.html}", Year = 1998, Abstract = "This is an FAQ to answer some basic questions arising from certain geometric computation in general dimensional (mostly Euclidean) space. The main areas to be covered are the convex hull computation of a finite point set, the vertex enumeration for a convex polytope, the computation of Voronoi diagram and Delaunay triangulation, in $R^d$. We illustrate typical solution processes with small examples and publicly available codes such as cdd+ and lrs.", } @InProceedings{FukudaP96, Author = "K. Fukuda and A. Prodon", Title = "Double Description Method Revisited", Booktitle = "Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5, 1995, Selected Papers", Editor = "M. Deza and R. Euler and Y. Manoussakis", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 1120, Pages = "91--111", Year = 1996, ISBN = "3-540-61576-8", Abstract = "The double description method is a simple and useful algorithm for enumerating all extreme rays of a general polyhedral cone in $R^d$, despite the fact that we can hardly state any interesting theorems on its time and space complexities. In this paper, we reinvestigate this method, introduce some new ideas for efficient implementations, and show some empirical results indicating its practicality in solving highly degenerate problems.", URL = "ftp://ftp.ifor.math.ethz.ch/pub/fukuda/reports/ddrev960315.ps.gz" } @InCollection{GawrilowJ00, Author = "E. Gawrilow and M. Joswig", Title = "{\tt polymake}: A Framework for Analyzing Convex Polytopes", Booktitle = "Polytopes - Combinatorics and Computation", Editor = "G. Kalai and G. M. Ziegler", Publisher = "Birkh{\"a}user", Pages = "43--74", Year = 2000, Abstract = "{\tt polymake} is a software tool designed for the algorithmic treatment of polytopes and polyhedra. We give an overview of the functionally as well as for the structure. This paper can be seen as a first approximation to a {\tt polymake} handbook. The tutorial starts with the very basic and ends with a few {\tt polymake} applications to research problems. Then we present the main features of the system including the interfaces to other software products." } @InProceedings{GawrilowJ01, Author = "E. Gawrilow and M. Joswig", Title = "{\tt polymake}: An Approach to Modular Software Design in Computational Geometry", Booktitle = "Proceedings of the 17th Annual Symposium on Computational Geometry", Organization = "ACM", Address = "Medford, MA, USA", Pages = "222--231", Year = 2001, Abstract = "{\tt polymake} is a software package designed for the study of the combinatorics and the geometry of convex polytopes and polyhedra. It offers access to a wide variety of algorithms and tools within a common framework. As a key design feature it allows to incorporate the functionality of a great variety of other software packages in a modular way." } @InProceedings{GopanDMDRS04, Author = "D. Gopan and F. DiMaio and N. Dor and T. W. Reps and M. Sagiv", Title = "Numeric Domains with Summarized Dimensions", Booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004", Address = "Barcelona, Spain", Editor = "K. Jensen and A. Podelski", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2988, Pages = "512--529", Year = 2004, ISBN = "3-540-21299-X", Abstract = "We introduce a systematic approach to designing summarizing abstract numeric domains from existing numeric domains. Summarizing domains use summary dimensions to represent potentially unbounded collections of numeric objects. Such domains are of benefit to analyses that verify properties of systems with an unbounded number of numeric objects, such as shape analysis, or systems in which the number of numeric objects is bounded, but large." } @InProceedings{Granger91, Author = "P. Granger", Title = "Static Analysis of Linear Congruence Equalities among Variables of a Program", Booktitle = "TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91)", Address = "Brighton, UK", Year = 1991, Editor = "S. Abramsky and T. S. E. Maibaum", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 493, ISBN = "3-540-53982-4", Pages = "169--192", Abstract = "In this paper, a new kind of static (or semantic) analysis is defined: congruence analysis, which is conceived to discover the properties of the following type: ``the integer valued variable $X$ is congruent to $c$ modulo $m$'', where $c$ and $m$ are automatically determined integers. This analysis is then related to an algebraic framework and wholly characterized. Moreover, we show an example how it can be useful for automatic vectorization. Finally, we present some extensions of it, namely its combination with the analysis of bounds, and also some analysis defined when the modulus of congruences is given \emph{a priori}.", } @InProceedings{Granger97, Author = "P. Granger", Title = "Static Analyses of Congruence Properties on Rational Numbers (Extended Abstract)", Booktitle = "Static Analysis: Proceedings of the 4th International Symposium", Address = "Paris, France", Year = 1997, Editor = "P. {Van Hentenryck}", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 1302, ISBN = "3-540-63468-1", Pages = "278--292", Abstract = "We present several new static analysis frameworks applying to rational numbers, and more precisely, designed for discovering congruence properties satisfied by rational (or real) variables of programs. Two of them deal with additive congruence properties and generalize linear equation analysis [M. Karr, \emph{Affine Relationships among Variables of a Program}, Acta Informatica, 6:133--151, 1976] and congruence analysis on integer numbers [P. Granger, \emph{Static Analysis of Arithmetical Congruences}, International Journal of Computer Mathematics, 30:165--190, 1989], [P. Granger, \emph{Static Analysis of Linear Congruence Equalities among Variables of a Program}, TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91), Lecture Notes in Computer Science, 493, pp. 169--192]. The others are based on multiplicative congruence properties in the set of positive rational numbers. Among other potential applications, we exemplify the interest of all these analyses for optimizing the representation of rational or real valued variables." } @Article{GoldfarbR77, Author = "D. Goldfarb and J. K. Reid", Title = "A Practical Steepest-Edge Simplex Algorithm", Journal = "Mathematical Proramming", Volume = 12, Number = 1, Pages = "361--371", Year = 1977, Abstract = "It is shown that suitable recurrences may be used in order to implement in practice the steepest-edge simplex linear programming algorithm. In this algorithm each iteration is along an edge of the polytope of feasible solutions on which the objective function decreases most rapidly with respect to distance in the space of all the variables. Results of computer comparisons on medium-scale problems indicate that the resulting algorithm requires less iterations but about the same overall time as the algorithm of Harris [8], which may be regarded as approximating the steepest-edge algorithm. Both show a worthwhile advantage over the standard algorithm." } @PhdThesis{Halbwachs79th, Author = "N. Halbwachs", Title = "D\'etermination Automatique de Relations Lin\'eaires V\'erifi\'ees par les Variables d'un Programme", Type = "{Th\`ese de 3\textsuperscript{\`eme} cycle d'informatique}", School = "Universit\'e scientifique et m\'edicale de Grenoble", Address = "Grenoble, France", Month = mar, Year = 1979 } @InProceedings{Halbwachs93, Author = "N. Halbwachs", Title = "Delay Analysis in Synchronous Programs", Pages = "333--346", Booktitle = "Computer Aided Verification: Proceedings of the 5th International Conference (CAV'93)", Address = "Elounda, Greece", Editor = "C. Courcoubetis", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 697, Year = 1993, ISBN = "3-540-56922-7", Abstract = "Linear relation analysis [CH78, Hal79] has been proposed a long time ago as an abstract interpretation which permits to discover linear relations invariantly satisfied by the variables of a program. Here, we propose to apply this general method to variables used to count delays in synchronous programs. The ``regular'' behavior of these counters makes the results of the analysis especially precise. These results can be applied to code optimization and to the verification of real-time properties of programs.", } @InProceedings{HalbwachsPR94, Author = "N. Halbwachs and Y.-E. Proy and P. Raymond", Title = "Verification of Linear Hybrid Systems by Means of Convex Approximations", Booktitle = "Static Analysis: Proceedings of the 1st International Symposium", Address = "Namur, Belgium", Editor = "B. {Le Charlier}", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 864, ISBN = "3-540-58485-4", Pages = "223--237", Year = 1994, Abstract = "We present 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. The result is an efficient automatic tool for approximate, but conservative, verification of reachability properties of these systems.", URL = "http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/hybrid.html" } @Manual{HalbwachsKP95, Author = "N. Halbwachs and A. Kerbrat and Y.-E. Proy", Title = "{POLyhedra INtegrated Environment}", Organization = "Verimag", Address = "France", Edition = "version 1.0 of {POLINE}", Month = sep, Year = 1995, Note = "documentation taken from source code", } @Article{HalbwachsPR97, Author = "N. Halbwachs and Y.-E. Proy and P. Roumanoff", Title = "Verification of Real-Time Systems using Linear Relation Analysis", Journal = "Formal Methods in System Design", Publisher = "Kluwer Academic Publishers", Volume = 11, Number = 2, Pages = "157--185", Year = 1997, Abstract = "Linear Relation Analysis [11] is an abstract interpretation devoted to the automatic discovery of invariant linear inequalities among numerical variables of a program. In this paper, we apply such an analysis to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.", } @Book{HenkinMT71, Author = "L. Henkin and J. D. Monk and A. Tarski", Title = "Cylindric Algebras: Part I", Publisher = "North-Holland", Address = "Amsterdam", ISBN = "978-0-7204-2043-2", Year = 1971, } @InProceedings{HenzingerH95, Author = "T. A. Henzinger and P.-H. Ho", Title = "A Note on Abstract Interpretation Strategies for Hybrid Automata", Booktitle = "Hybrid Systems II", Editor = "P. J. Antsaklis and W. Kohn and A. Nerode and S. Sastry", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 999, Pages = "252--264", Year = 1995, Abstract = "We report on several abstract interpretation strategies that are designed to improve the performance of {\sc HyTech}, a symbolic model checker for linear hybrid systems. We (1) simultaneously compute the target region from different directions, (2) conservatively approximate the target region by dropping constraints, and (3) iteratively refine the approximation until sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.", URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/abstract-interpretation_strategies_for_hybrid_automata.html" } @InProceedings{HenzingerPW01, Author = "T. A. Henzinger and J. Preussig and H. Wong-Toi", Title = "Some Lessons from the {\sc HyTech} Experience", Booktitle = "Proceedings of the 40th Annual Conference on Decision and Control", Publisher = "IEEE Computer Society Press", Pages = "2887--2892", Year = 2001, Abstract = "We provide an overview of the current status of the tool {\sc HyTech}, and reflect on some of the lessons learned from our experiences with the tool. HyTech is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.", URL = "http://www-cad.eecs.berkeley.edu/HomePages/tah/Publications/some_lessons_from_the_hytech_experience.html" } @TechReport{HuelsbergenHL90, Author = "L. Huelsbergen and D. Hahn and J. Larus", Title = "Exact Dependence Analysis Using Data Access Descriptors", Number = 945, Institution = "Department of Computer Science, University of Wisconsin", Address = "Madison", Year = 1990, Abstract = "\emph{Data Access Descriptors} provide a method for summarizing and representing the portion of an array accessed by a program statement. A Data Access Descriptor does not, however, indicate if its characterization is exact or conservative, nor does it record the temporal order of accesses. Exactness is necessary to expose maximal parallelism. Temporal information is necessary to calculate \emph{direction vectors} for inter-loop dependences. This paper presents an extension to basic Data Access Descriptors that identies exact representations. We illustrate the value of extended Data Access Descriptors by showing how to calculate information typically provided by direction vectors and by refining potential conflicts between statements with \emph{array kill} information." } @InProceedings{JaffarMSY94, Author = "J. Jaffar and M. J. Maher and P. J. Stuckey and R. H. C. Yap", Title = "Beyond Finite Domains", Booktitle = "Principles and Practice of Constraint Programming: Proceedings of the Second International Workshop", Publisher = "Springer-Verlag, Berlin", Editor = "A. Borning", Address = "Rosario, Orcas Island, Washington, USA", Series = "Lecture Notes in Computer Science", Volume = 874, Pages = "86--94", Year = 1994, } @Article{KhachiyanBBEG06, Author = "L. Khachiyan and E. Boros and K. Borys and K. Elbassioni and V. Gurvich", Title = "Generating All Vertices of a Polyhedron Is Hard", Journal = "Discrete and Computational Geometry", Publisher = "Springer", Address = "New York", Year = 2006, Note = "Invited contribution. To appear.", Abstract = "We show that generating all negative cycles of a weighted graph is a hard enumeration problem, in both the directed and undirected cases. More precisely, given a family of such cycles, it is NP-complete problem to decide whether this family can be extended or there is no other negative directed cycles in the graph, implying that directed negative cycles cannot be generated in polynomial output time, unless P=NP. As a corollary, we solve in the negative two well-known generating problems from linear programming: (i) Given an (infeasible) system of linear inequalities, generating all minimal infeasible subsystems is hard. Yet, for generating maximal feasible subsystems the complexity remains open. (ii) Given a (feasible) system of linear inequalities, generating all vertices of the corresponding polyhedron is hard. Yet, in case of bounded polyhedra the complexity remains open." } @Inproceedings{NakanishiJPF99, Author = "T. Nakanishi and K. Joe and C. D. Polychronopoulos and A. Fukuda", Title = "The Modulo Interval: A Simple and Practical Representation for Program Analysis", Booktitle = "Proceedings of the 1999 International Conference on Parallel Architectures and Compilation Techniques", Address = "Newport Beach, California, USA", Publisher = "IEEE Computer Society", Year = 1999, Pages = "91--96", Abstract = "In this paper, the modulo interval, an extension of the traditional interval on real numbers, and its useful mathematical properties are presented as a representation for program analysis Only with two additional parameters to the interval on real numbers, namely the modulus and the residue, the modulo interval can represent information on program having cyclicity such as loop indices, array subscripts etc. at reasonable complexity and more accuracy. Well-defined arithmetic and set operations on the modulo interval make implementation of compilers simple and reliable. Moreover, application of the modulo interval to program analysis for parallelizing compilers is discussed in this paper." } @Article{NakanishiF01, Author = "T. Nakanishi and A. Fukuda", Title = "Modulo Interval Arithmetic and Its Application to Program Analysis", Journal = "Transactions of Information Processing Society of Japan", Volume = 42, Number = 4, Pages = "829--837", Year = 2001, } @Manual{NEW-POLKA-1-1-3c, Author = "B. Jeannet", Title = "Convex Polyhedra Library", Edition = "release 1.1.3c", Month = mar, Year = 2002, Note = "documentation of the ``New Polka'' library.", } @Article{Kuhn56, Author = "H. W. Kuhn", Title = "Solvability and Consistency for Linear Equations and Inequalities", Journal = "American Mathematical Monthly", Volume = 63, Pages = "217--232", Year = 1956, } @TechReport{LeVerge92, Author = "H. {Le Verge}", Title = "A note on {Chernikova's} Algorithm", Type = "\emph{Publication interne}", Number = 635, Institution = "IRISA", Address = "Campus de Beaulieu, Rennes, France", Year = 1992, Abstract = "This paper describes 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. This algorithm can also be used for the dual problem: given a set of extremal rays and vertices, find the associated irredundant set of facet supporting hyperplanes. The method is an extension of initial Chernikova's algorithm (non negative domain), and is mainly based on the polyhedral cone duality principle. A new enhancement for extremal ray detection together with its effects on a class of polyhedra.", Source = "chernikova.c" } @TechReport{LeVergeVDW94, Author = "H. {Le Verge}, V. {Van Dongen} and D. K. Wilde", Title = "Loop Nest Synthesis Using the Polyhedral Library", Type = "\emph{Publication interne}", Number = 830, Institution = "IRISA", Address = "Campus de Beaulieu, Rennes, France", Year = 1994, Abstract = "A new method to synthesis loop nests given a polyhedral domain, the context domain, and the loop nesting order is described. The method is based on functions in the IRISA polyhedral library." } @Article{LoechnerW97, Author = "V. Loechner and D. K. Wilde", Title = "Parameterized Polyhedra and Their Vertices", Journal = "International Journal of Parallel Programming", Volume = 25, Number = 6, Pages = "525--549", Year = 1997, Abstract = "Algorithms specified for parametrically sized problems are more general purpose and more reusable than algorithms for fixed sized problems. For this reason, there is a need for representing and symbolically analyzing linearly parameterized algorithms. An important class of parallel algorithms can be described as systems of parameterized affine recurrence equations (PARE). In this representation, linearly parameterized polyhedra are used to described the domains of variables. This paper describes an algorithm which computes the set of parameterized vertices of a polyhedron, given its representation as a system of parameterized inequalities. This provides an important tool for the symbolic analysis of the parameterized domains used to define variables and computation domains in PARE's. A library of operations on parameterized polyhedra based on the Polyhedral Library has been written in C and is freely distributed." } @Misc{Loechner99, Author = "V. Loechner", Title = "{\it PolyLib\/}: A Library for Manipulating Parameterized Polyhedra", Howpublished = "Available at \url{http://icps.u-strasbg.fr/~loechner/polylib/}", Year = 1999, Month = mar, Note = "Declares itself to be a continuation of \cite{Wilde93th}" } @InProceedings{Masdupuy92, Author = "F. Masdupuy", Title = "Array Operations Abstraction Using Semantic Analysis of Trapezoid Congruences", Booktitle = "Proceedings of the 6th ACM International Conference on Supercomputing", Address = "Washington, DC, USA", Publisher = "ACM Press", Pages = "226--235", Year = 1992, Abstract = "With the growing use of vector supercomputers, efficient and accurate data structure analyses are needed. What we propose in this paper is to use the quite general framework of Cousot's abstract interpretation for the particular analysis of multi-dimensional array indexes. While such indexes are integer tuples, a relational integer analysis is first required. This analysis results of a combination of existing ones that are interval and congruence based. Two orthogonal problems are directly concerned with the results of such an analysis, that are the parallelization/vectorization with the dependence analysis and the data locality problem used for array storage management. After introducing the analysis algorithm, this paper describes on a complete example how to use it in order to optimize array storage." } @PhdThesis{Masdupuy93th, Author = "F. Masdupuy", Title = "Array Indices Relational Semantic Analysis Using Rational Cosets and Trapezoids", Type = "{Th\`ese d'informatique}", School = "\'Ecole Polytechnique", Address = "Palaiseau, France", Month = dec, Year = 1993, Abstract = "Semantic analysis of program numerical variables consists in statically and automatically discovering properties verified at execution time. Different sets of properties (equality, inequality and congruence relations) have already been studied. This thesis proposes a generalization of some of the below patterns. More specifically, the abstract interpretation is used to design on the one hand a set of properties generalizing intervals and cosets on $\mathbbb{Z}$ and on the other hand, a generalization of trapezoids and linear congruence equation systems on $\mathbbb{Z}^n$. A rational abstraction of these properties is defined to get safe approximations, with a polynomial complexity in the number of the considered variables, of the integer properties operators. Those analyses, more precise than the combination of the analysis they come from in general, allow to dynamically choose the kind of properties (inequality or congruence relations) leading to relevant information for the considered program. The described relationnal analysis corresponds to numerous patterns encountered in the field of scientific computation. It is very well adapted to the analysis of array indices variables and also to the abstract description of integer arrays." } @InProceedings{Mine01a, Author = "A. Min\'e", Title = "A New Numerical Abstract Domain Based on Difference-Bound Matrices", Booktitle = "Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001)", Address = "Aarhus, Denmark", Editor = "O. Danvy and A. Filinski", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2053, Pages = "155--172", Year = 2001, Abstract = "This paper presents a new numerical domain for static analysis by abstract interpretation. This domain allows us to represent invariants of the form and , where and are variables values and is an integer or real constant. Abstract elements are represented by Difference-Bound Matrices, widely used by model-checkers, but we had to design new operators to meet the needs of abstract interpretation. The result is a complete lattice of infinite height featuring widening, narrowing and common transfer functions. We focus on giving an efficient representation and graph-based algorithms---where is the number of variables---and claim that this domain always performs more precisely than the well-known interval domain. To illustrate the precision/cost tradeoff of this domain, we have implemented simple abstract interpreters for toy imperative and parallel languages which allowed us to prove some non-trivial algorithms correct." } @InProceedings{Mine01b, Author = "A. Min\'e", Title = "The Octagon Abstract Domain", Booktitle = "Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01)", Address = "Stuttgart, Germany", Year = 2001, Publisher = "IEEE Computer Society Press", Pages = "310--319", Abstract = "This article presents a new numerical abstract domain for static analysis by abstract interpretation. It extends our previously proposed DBM-based numerical abstract domain and allows us to represent invariants of the form ($\pm x \pm y \leq c$), where $x$ and $y$ are program variables and $c$ is a real constant. We focus on giving an efficient representation based on Difference-Bound Matrices---$\mathcal{O}(n^2)$ memory cost, where $n$ is the number of variables---and graph-based algorithms for all common abstract operators---$\mathcal{O}(n^3)$ time cost. This includes a normal form algorithm to test equivalence of representation and a widening operator to compute least fixpoint approximations." } @InProceedings{Mine02, Author = "A. Min\'e", Title = "A Few Graph-Based Relational Numerical Abstract Domains", Booktitle = "Static Analysis: Proceedings of the 9th International Symposium", Address = "Madrid, Spain", Editor = "M. V. Hermenegildo and G. Puebla", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2477, ISBN = "3-540-44235-9", Pages = "117--132", Year = 2002, Abstract = "This article presents the systematic design of a class of relational numerical abstract domains from non-relational ones. Constructed domains represent sets of invariants of the form $(v_j-v_i\in C)$, where vj and vi are two variables, and $C$ lives in an abstraction of $\mathcal{P}(\mathbb {Z})$, $\mathcal{P}(\mathbb {Q})$, or $\mathcal{P}(\mathbb {R})$. We will call this family of domains weakly relational domains. The underlying concept allowing this construction is an extension of potential graphs and shortest-path closure algorithms in exotic-like algebras. Example constructions are given in order to retrieve well-known domains as well as new ones. Such domains can then be used in the Abstract Interpretation framework in order to design various static analyses. A major benefit of this construction is its modularity, allowing to quickly implement new abstract domains from existing ones." } @InProceedings{Mine04, Author = "A. Min\'e", Title = "Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors", Booktitle = "Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming", Address = "Barcelona, Spain", Editor = "D. Schmidt", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 2986, ISBN = "3-540-213213-9", Year = 2004, Pages = "3--17", Abstract = "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." } @PhdThesis{Mine05th, Author = "A. Min\'e", Title = "Weakly Relational Numerical Abstract Domains", School = "\'Ecole Polytechnique", Address = "Paris, France", Month = mar, Year = 2005, Abstract = "The goal of this thesis is to design techniques related to the automatic analysis of computer programs. One major application is the creation of tools to discover bugs before they actually happen, an important goal in a time when critical yet complex tasks are performed by computers. We will work in the Abstract Interpretation framework, a theory of sound approximations of program semantics. We will focus, in particular, on numerical abstract domains that specialise in the automatic discovery of properties of the numerical variables of programs. In this thesis, we introduce new numerical abstract domains: the zone abstract domain (that can discover invariants of the form $X - Y \leq c$), the zone congruence domain ($X \equiv Y + a [b]$), and the octagon domain ($\pm X \pm Y \leq c$), among others. These domains rely on the classical notions of potential graphs, difference bound matrices, and algorithms for the shortest-path closure computation. They are in-between, in terms of cost and precision, between nonrelational domains (such as the interval domain), that are very imprecise, and classical relational domains (such as the polyhedron domain), that are very costly. We will call them ``weakly relational''. We also introduce some methods to apply relational domains to the analysis of floating-point numbers, which was previously only possible using imprecise, non-relational, domains. Finally, we introduce the so-called linearisation and symbolic constant propagation generic symbolic methods to enhance the precision of any numerical domain, for only a slight increase in cost. The techniques presented in this thesis have been integrated within Astr\'ee, an analyser for critical embedded avionic software, and were instrumental in proving the absence of run-time errors in fly-by-wire softwares used in Airbus A340 and A380 planes. Experimental results show the usability of our methods of real-life applications.", } @InCollection{MotzkinRTT53, Author = "T. S. Motzkin and H. Raiffa and G. L. Thompson and R. M. Thrall", Title = "The Double Description Method", Booktitle = "Contributions to the Theory of Games -- Volume II", Editor = "H. W. Kuhn and A. W. Tucker", Series = "Annals of Mathematics Studies", Number = 28, Publisher = "Princeton University Press", Address = "Princeton, New Jersey", Year = 1953, Pages = "51--73", Abstract = "The purpose of this paper is to present a computational method for the determination of the value and of all solutions of a two-person zero-sum game with a finite number of pure strategies, and for the solution of general finite systems of linear inequalities and corresponding maximization problems." } @InProceedings{NelsonO77, Author = "G. Nelson and D. C. Oppen", Title = "Fast Decision Algorithms based on {Union} and {Find}", Booktitle = "Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS'77)", Address = "Providence, RI, USA", Publisher = "IEEE Computer Society Press", Pages = "114--119", Year = 1977, Note = "The journal version of this paper is \cite{NelsonO80}" } @Article{NelsonO80, Author = "G. Nelson and D. C. Oppen", Title = "Fast Decision Procedures Based on Congruence Closure", Journal = "Journal of the ACM", Publisher = "ACM Press", Volume = 27, Number = 2, Pages = "356--364", Year = 1980, Note = "An earlier version of this paper is \cite{NelsonO77}", Abstract = "The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length n in average time $O(n \log n)$ using the fastest known congruence closure algorithm. It is also shown that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier." } @Book{NemhauserW88, Author = "G. L. Nemhauser and L. A. Wolsey", Title = "Integer and Combinatorial Optimization", Publisher = "John Wiley \& Sons", Series = "Wiley Interscience Series in Discrete Mathematics and Optimization", Year = 1988 } @TechReport{NookalaR00, Author = "S. P. K. Nookala and T. Risset", Title = "A Library for {Z}-Polyhedral Operations", Type = "\emph{Publication interne}", Number = 1330, Institution = "IRISA", Address = "Campus de Beaulieu, Rennes, France", Year = 2000, Abstract = "Polyhedra are commonly used for representing iteration domains of loop nests with unit stride: the iteration domain of a loop is associated with the set of integer points contained in a polyhedron. ${\cal Z}$-polyhedra are natural extension of polyhedra, in the sense that they represent iteration domains of loop nests with non-unit stride (they are polyhedra intersected with integral lattices). The polyhedral library (Polylib) has been developed for computing on polyhedra, it is now widely used in the automatic parallelization research community. This report describes the implementation of the extension of Polylib to ${\cal Z}$-polyhedra. We describe algorithms used for computing on lattices and ${\cal Z}$-polyhedra, and we provide technical documentation for the ${\cal Z}$-polyhedral library (data structures, functions available)." } @Book{PapadimitriouS98, Author = "C. H. Papadimitriou and K. Steiglitz", Title = "Combinatorial Optimization: Algorithms and Complexity", Edition = "Second", Publisher = "Dover Publications", ISBN = "0-486-40258-4", Year = 1998, } @Unpublished{Pratt77, Author = "V. R. Pratt", Title="Two Easy Theories whose Combination is Hard", Note = "Memo sent to Nelson and Oppen concerning a preprint of their paper \cite{NelsonO77}", Month = sep, Year = 1977, Abstract = "We restrict attention to the validity problem for unquantified disjunctions of literals (possibly negated atomic formulae) over the domain of integers, or what is just as good, the satisfiability problem for unquantified conjunctions. When $=$ is the only predicate symbol and all function symbols are left uninterpreted, or when $\geq$ is the only predicate symbol (taking its standard interpretation on the integers) and the only terms are variables and integers, then satisfiability is decidable in polynomial time. However when $\geq$ and uninterpreted function symbols are allowed to appear together, satisfiability becomes an NP-complete problem. This combination of the two theories can arise for example when reasoning about arrays (the uninterpreted function symbols) and subscript manipulation (where $\geq$ arises in considering subscript bounds). These results are unaffected by the presence of successor, which also arises commonly in reasoning about subscript manipulation." } @Article{QuillereRW00, Author = "F. Quiller{\'e} and S. V. Rajopadhye and D. Wilde", Title = "Generation of Efficient Nested Loops from Polyhedra", Journal = "International Journal of Parallel Programming", Volume = 28, Number = 5, Year = 2000, Pages = "469--498", Abstract = "Automatic parallelization in the polyhedral model is based on affine transformations from an original computation domain (iteration space) to a target space-time domain, often with a different transformation for each variable. Code generation is an often ignored step in this process that has a significant impact on the quality of the final code. It involves making a trade-off between code size and control code simplification/optimization. Previous methods of doing code generation are based on loop splitting, however they have nonoptimal behavior when working on parameterized programs. We present a general parameterized method for code generation based on dual representation of polyhedra. Our algorithm uses a simple recursion on the dimensions of the domains, and enables fine control over the tradeoff between code size and control overhead." } @TechReport{QuintonRR96, Author = "P. Quinton and S. Rajopadhye and T. Risset", Title = "On Manipulating {Z}-Polyhedra", Year = 1996, Month = jul, Institution = "IRISA, Campus Universitaire de Bealieu, Rennes, France", Number = 1016, Abstract = "We address the problem of computation upon Z-Polyhedra which are intersections of polyhedra and integral lattices. We introduce a canonic representation for Z-polyhedra which allow to perform comparisons and transformations of Z-polyhedra with the help of a computational kernal on polyhedra. This contribution is a step towards the manipulation of images of polyhedra by affine functions, and has application in the domain of automatic parallelization and parallel VLSI synthesis.", } @Article{QuintonRR97, Author = "P. Quinton and S. Rajopadhye and T. Risset", Title = "On Manipulating {Z}-Polyhedra Using a Canonic Representation", Journal = "Parallel Processing Letters", Publisher = "World Scientific Publishing Company", Volume = 7, Number = 2, Pages = "181--194", Year = 1997, Abstract = "Z-Polyhedra are intersections of polyhedra and integral lattices. They arise in the domain of automatic parallelization and VLSI array synthesis. In this paper, we address the problem of computation on Z-polyhedra. We introduce a canonical representation for Z-polyhedra which allows one to perform comparisons and transformations of Z-polyhedra with the help of a computational kernal on polyhedra.", } @Inproceedings{RepsBL06, Author = "T. W. Reps and G. Balakrishnan and J. Lim", Title = "Intermediate-representation Recovery from Low-level Code", Booktitle = "Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation", Address = "Charleston, South Carolina, USA", Editor = "J. Hatcliff and F. Tip", Publisher = "ACM Press", ISBN = "1-59593-196-1", Year = 2006, Pages = "100--111", Abstract = "The goal of our work is to create tools that an analyst can use to understand the workings of COTS components, plugins, mobile code, and DLLs, as well as memory snapshots of worms and virus-infected code. This paper describes how static analysis provides techniques that can be used to recover intermediate representations that are similar to those that can be created for a program written in a high-level language." } @MastersThesis{Ricci02th, Author = "E. Ricci", Title = "Rappresentazione e manipolazione di poliedri convessi per l'analisi e la verifica di programmi", Type = "Laurea dissertation", School = "University of Parma", Address = "Parma, Italy", Month = jul, Year = 2002, Note = "In Italian", URL = "http://bugseng.com/products/ppl/documentation/Ricci02th.pdf" } @Inproceedings{SenS07, Author = "R. Sen and Y. N. Srikant", Title = "Executable Analysis using Abstract Interpretation with Circular Linear Progressions", Booktitle = "Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007)", Address = "Nice, France", Publisher = "IEEE Computer Society Press", Year = 2007, Pages = "39--48", Abstract = "We propose a new abstract domain for static analysis of executable code. Concrete states are abstracted using Circular Linear Progressions (CLPs). CLPs model computations using a finite word length as is seen in any real life processor. The finite abstraction allows handling over-flow scenarios in a natural and straight-forward manner. Abstract transfer functions have been defined for a wide range of operations which makes this domain easily applicable for analyzing code for a wide range of ISAs. CLPs combine the scalability of interval domains with the discreteness of linear congruence domains. We also present a novel, lightweight method to track linear equality relations between static objects that is used by the analysis to improve precision. The analysis is efficient, the total space and time overhead being quadratic in the number of static objects being tracked." } @Techreport{SenS07TR, Author = "R. Sen and Y. N. Srikant", Title = "Executable Analysis with Circular Linear Progressions", Number = "IISc-CSA-TR-2007-3", Institution = "Department of Computer Science and Automation, Indian Institute of Science", Address = "Bangalore, India", Year = 2007, Abstract = "We propose a new abstract domain for static analysis of executable code. Concrete state is abstracted using Circular Linear Progressions (CLPs). CLPs model computations using a finite word length as is seen in any real life processor. The finite abstraction allows handling overflow scenarios in a natural and straight-forward manner. Abstract transfer functions have been defined for a wide range of operations which makes this domain easily applicable for analysing code for a wide range of ISAs. CLPs combine the scalability of interval domains with the discreteness of linear congruence domains. We also present a novel, lightweight method to track linear equality relations between static objects that is used by the analysis to improve precision. The analysis is efficient, the total space and time overhead being quadratic in the number of static objects being tracked." } @Article{Shostak81, Author = "R. E. Shostak", Title = "Deciding Linear Inequalities by Computing Loop Residues", Journal = "Journal of the ACM", Publisher = "ACM Press", Volume = 28, Number = 4, Pages = "769--779", Year = 1981, Abstract = "V.~R.~Pratt has shown that the real and integer feasibility of sets of linear inequalities of the form $x \leq y + c$ can be decided quickly by examining the loops in certain graphs. Pratt's method is generalized, first to real feasibility of inequalities in two variables and arbitrary coefficients, and ultimately to real feasibility of arbitrary sets of linear inequalities. The method is well suited to applications in program verification." } @Book{Schrijver99, Author = "A. Schrijver", Title = "Theory of Linear and Integer Programming", Publisher = "John Wiley \& Sons", Series = "Wiley Interscience Series in Discrete Mathematics and Optimization", ISBN = "0-471-98232-6", Year = 1999 } @InProceedings{SimonK07, Author = "A. Simon and A. King", Title = "Taming the Wrapping of Integer Arithmetic", Booktitle = "Static Analysis: Proceedings of the 14th International Symposium", Address = "Kongens Lyngby, Denmark", Editor = "H. {Riis Nielson} and G. Fil{\'e}", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 4634, ISBN = "978-3-540-74060-5", Year = 2007, Pages = "121--136", Abstract = "Variables in programs are usually confined to a fixed number of bits and results that require more bits are truncated. Due to the use of 32-bit and 64-bit variables, inadvertent overflows are rare. However, a sound static analysis must reason about overflowing calculations and conversions between unsigned and signed integers; the latter remaining a common source of subtle programming errors. Rather than polluting an analysis with the low-level details of modelling two's complement wrapping behaviour, this paper presents a computationally light-weight solution based on polyhedral analysis which eliminates the need to check for wrapping when evaluating most (particularly linear) assignments." } @Article{Srivastava93, Author = "D. Srivastava", Title = "Subsumption and Indexing in Constraint Query Languages with Linear Arithmetic Constraints", Journal = "Annals of Mathematics and Artificial Intelligence", Volume = 8, Number = "3--4", Pages = "315--343", Year = 1993, Abstract = "Bottom-up evaluation of a program-query pair in a constraint query language (CQL) starts with the facts in the database and repeatedly applies the rules of the program, in iterations, to compute new facts, until we have reached a fixpoint. Checking if a fixpoint has been reached amounts to checking if any ``new'' facts were computed in an iteration. Such a check also enhances efficiency in that subsumed facts can be discarded, and not be used to make any further derivations in subsequent iterations, if we use Semi-naive evaluation. We show that the problem of subsumption in CQLs with linear arithmetic constraints is co-NP complete, and present a deterministic algorithm, based on the divide and conquer strategy, for this problem. We also identify polynomial-time sufficient conditions for subsumption and non-subsumption in CQLs with linear arithmetic constraints. We adapt indexing strategies from spatial databases for efficiently indexing facts in such a CQL: such indexing is crucial for performance in the presence of large databases. Based on a recent algorithm by Lassez and Lassez [LL] for quantifier elimination, we present an incremental version of the algorithm to check for subsumption in CQLs with linear arithmetic constraints.", URL = "http://www.research.att.com/~divesh/papers/s93-cqlsubsum-journal.ps" } @Book{StoerW70, Author = "J. Stoer and C. Witzgall", Title = "Convexity and Optimization in Finite Dimensions {I}", Publisher = "Springer-Verlag, Berlin", Year = 1970 } @Book{Warren03, Author = "Warren, Jr., H. S.", Title = "Hacker's Delight", Publisher = "Addison-Wesley Longman Publishing Co., Inc.", Address = "Boston, MA, USA", Year = 2003, ISBN = "0-201-91465-4", } @MastersThesis{Wilde93th, Author = "D. K. Wilde", Title = "A Library for Doing Polyhedral Operations", Type = "{Master's thesis}", School = "Oregon State University", Address = "Corvallis, Oregon", Month = dec, Year = 1993, Note = "Also published as IRISA \emph{Publication interne} 785, Rennes, France, 1993", Abstract = "Polyhedra are geometric representations of linear systems of equations and inequalities. Since polyhedra are used to represent the iteration domains of nested loop programs, procedures for operating on polyhedra are useful for doing loop transformations and other program restructuring transformations which are needed in parallelizing compilers. Thus a need for a library of polyhedral operations has recently been recognized in the parallelizing compiler community. Polyhedra are also used in the definition of domains of variables in systems of affine recurrence equations (SARE). {\sc Alpha} is a language which is based on the SARE formalism in which all variables are declared over finite unions of polyhedra. This report describes a library of polyhedral functions which was developed to support the {\sc Alpha} language environment, and which is general enough to satisfy the needs of researchers doing parallelizing compilers. This report describes the data structures used to represent domains, gives motivations for the major design decisions, and presents the algorithms used for doing polyhedral operations. This library has been written and tested, and has been in use since the beginning of 1993 by research facilities in Europe and Canada. The library is freely distributed by ftp.", URL = "http://www.irisa.fr/polylib/document/Polylib.ps" } @Article{Weyl35, Author = "H. Weyl", Title = "Elementare Theorie der konvexen Polyeder", Journal = "Commentarii Mathematici Helvetici", Publisher = "{Birkh\"auser} Publishing Ltd., Basel, Switzerland", Volume = 7, Pages = "290--306", Year = 1935, Note = "English translation in \cite{Weyl50}" } @InCollection{Weyl50, Author = "H. Weyl", Title = "The Elementary Theory of Convex Polyhedra", Booktitle = "Contributions to the Theory of Games -- Volume I", Editor = "H. W. Kuhn", Series = "Annals of Mathematics Studies", Number = 24, Publisher = "Princeton University Press", Address = "Princeton, New Jersey", Year = 1950, Pages = "3--18", Note = "Translated from \cite{Weyl35} by H. W. Kuhn" } ==============================================================================

ODC Attribution License (ODC-By)

### Preamble The Open Data Commons Attribution License is a license agreement intended to allow users to freely share, modify, and use this Database subject only to the attribution requirements set out in Section 4. Databases can contain a wide variety of types of content (images, audiovisual material, and sounds all in the same database, for example), and so this license only governs the rights over the Database, and not the contents of the Database individually. Licensors may therefore wish to use this license together with another license for the contents. Sometimes the contents of a database, or the database itself, can be covered by other rights not addressed here (such as private contracts, trademark over the name, or privacy rights / data protection rights over information in the contents), and so you are advised that you may have to consult other documents or clear other rights before doing activities not covered by this License. ------ The Licensor (as defined below) and You (as defined below) agree as follows: ### 1.0 Definitions of Capitalised Words "Collective Database" - Means this Database in unmodified form as part of a collection of independent databases in themselves that together are assembled into a collective whole. A work that constitutes a Collective Database will not be considered a Derivative Database. "Convey" - As a verb, means Using the Database, a Derivative Database, or the Database as part of a Collective Database in any way that enables a Person to make or receive copies of the Database or a Derivative Database. Conveying does not include interaction with a user through a computer network, or creating and Using a Produced Work, where no transfer of a copy of the Database or a Derivative Database occurs. "Contents" - The contents of this Database, which includes the information, independent works, or other material collected into the Database. For example, the contents of the Database could be factual data or works such as images, audiovisual material, text, or sounds. "Database" - A collection of material (the Contents) arranged in a systematic or methodical way and individually accessible by electronic or other means offered under the terms of this License. "Database Directive" - Means Directive 96/9/EC of the European Parliament and of the Council of 11 March 1996 on the legal protection of databases, as amended or succeeded. "Database Right" - Means rights resulting from the Chapter III ("sui generis") rights in the Database Directive (as amended and as transposed by member states), which includes the Extraction and Re-utilisation of the whole or a Substantial part of the Contents, as well as any similar rights available in the relevant jurisdiction under Section 10.4. "Derivative Database" - Means a database based upon the Database, and includes any translation, adaptation, arrangement, modification, or any other alteration of the Database or of a Substantial part of the Contents. This includes, but is not limited to, Extracting or Re-utilising the whole or a Substantial part of the Contents in a new Database. "Extraction" - Means the permanent or temporary transfer of all or a Substantial part of the Contents to another medium by any means or in any form. "License" - Means this license agreement and is both a license of rights such as copyright and Database Rights and an agreement in contract. "Licensor" - Means the Person that offers the Database under the terms of this License. "Person" - Means a natural or legal person or a body of persons corporate or incorporate. "Produced Work" - a work (such as an image, audiovisual material, text, or sounds) resulting from using the whole or a Substantial part of the Contents (via a search or other query) from this Database, a Derivative Database, or this Database as part of a Collective Database. "Publicly" - means to Persons other than You or under Your control by either more than 50% ownership or by the power to direct their activities (such as contracting with an independent consultant). "Re-utilisation" - means any form of making available to the public all or a Substantial part of the Contents by the distribution of copies, by renting, by online or other forms of transmission. "Substantial" - Means substantial in terms of quantity or quality or a combination of both. The repeated and systematic Extraction or Re-utilisation of insubstantial parts of the Contents may amount to the Extraction or Re-utilisation of a Substantial part of the Contents. "Use" - As a verb, means doing any act that is restricted by copyright or Database Rights whether in the original medium or any other; and includes without limitation distributing, copying, publicly performing, publicly displaying, and preparing derivative works of the Database, as well as modifying the Database as may be technically necessary to use it in a different mode or format. "You" - Means a Person exercising rights under this License who has not previously violated the terms of this License with respect to the Database, or who has received express permission from the Licensor to exercise rights under this License despite a previous violation. Words in the singular include the plural and vice versa. ### 2.0 What this License covers 2.1. Legal effect of this document. This License is: a. A license of applicable copyright and neighbouring rights; b. A license of the Database Right; and c. An agreement in contract between You and the Licensor. 2.2 Legal rights covered. This License covers the legal rights in the Database, including: a. Copyright. Any copyright or neighbouring rights in the Database. The copyright licensed includes any individual elements of the Database, but does not cover the copyright over the Contents independent of this Database. See Section 2.4 for details. Copyright law varies between jurisdictions, but is likely to cover: the Database model or schema, which is the structure, arrangement, and organisation of the Database, and can also include the Database tables and table indexes; the data entry and output sheets; and the Field names of Contents stored in the Database; b. Database Rights. Database Rights only extend to the Extraction and Re-utilisation of the whole or a Substantial part of the Contents. Database Rights can apply even when there is no copyright over the Database. Database Rights can also apply when the Contents are removed from the Database and are selected and arranged in a way that would not infringe any applicable copyright; and c. Contract. This is an agreement between You and the Licensor for access to the Database. In return you agree to certain conditions of use on this access as outlined in this License. 2.3 Rights not covered. a. This License does not apply to computer programs used in the making or operation of the Database; b. This License does not cover any patents over the Contents or the Database; and c. This License does not cover any trademarks associated with the Database. 2.4 Relationship to Contents in the Database. The individual items of the Contents contained in this Database may be covered by other rights, including copyright, patent, data protection, privacy, or personality rights, and this License does not cover any rights (other than Database Rights or in contract) in individual Contents contained in the Database. For example, if used on a Database of images (the Contents), this License would not apply to copyright over individual images, which could have their own separate licenses, or one single license covering all of the rights over the images. ### 3.0 Rights granted 3.1 Subject to the terms and conditions of this License, the Licensor grants to You a worldwide, royalty-free, non-exclusive, terminable (but only under Section 9) license to Use the Database for the duration of any applicable copyright and Database Rights. These rights explicitly include commercial use, and do not exclude any field of endeavour. To the extent possible in the relevant jurisdiction, these rights may be exercised in all media and formats whether now known or created in the future. The rights granted cover, for example: a. Extraction and Re-utilisation of the whole or a Substantial part of the Contents; b. Creation of Derivative Databases; c. Creation of Collective Databases; d. Creation of temporary or permanent reproductions by any means and in any form, in whole or in part, including of any Derivative Databases or as a part of Collective Databases; and e. Distribution, communication, display, lending, making available, or performance to the public by any means and in any form, in whole or in part, including of any Derivative Database or as a part of Collective Databases. 3.2 Compulsory license schemes. For the avoidance of doubt: a. Non-waivable compulsory license schemes. In those jurisdictions in which the right to collect royalties through any statutory or compulsory licensing scheme cannot be waived, the Licensor reserves the exclusive right to collect such royalties for any exercise by You of the rights granted under this License; b. Waivable compulsory license schemes. In those jurisdictions in which the right to collect royalties through any statutory or compulsory licensing scheme can be waived, the Licensor waives the exclusive right to collect such royalties for any exercise by You of the rights granted under this License; and, c. Voluntary license schemes. The Licensor waives the right to collect royalties, whether individually or, in the event that the Licensor is a member of a collecting society that administers voluntary licensing schemes, via that society, from any exercise by You of the rights granted under this License. 3.3 The right to release the Database under different terms, or to stop distributing or making available the Database, is reserved. Note that this Database may be multiple-licensed, and so You may have the choice of using alternative licenses for this Database. Subject to Section 10.4, all other rights not expressly granted by Licensor are reserved. ### 4.0 Conditions of Use 4.1 The rights granted in Section 3 above are expressly made subject to Your complying with the following conditions of use. These are important conditions of this License, and if You fail to follow them, You will be in material breach of its terms. 4.2 Notices. If You Publicly Convey this Database, any Derivative Database, or the Database as part of a Collective Database, then You must: a. Do so only under the terms of this License; b. Include a copy of this License or its Uniform Resource Identifier (URI) with the Database or Derivative Database, including both in the Database or Derivative Database and in any relevant documentation; c. Keep intact any copyright or Database Right notices and notices that refer to this License; and d. If it is not possible to put the required notices in a particular file due to its structure, then You must include the notices in a location (such as a relevant directory) where users would be likely to look for it. 4.3 Notice for using output (Contents). Creating and Using a Produced Work does not require the notice in Section 4.2. However, if you Publicly Use a Produced Work, You must include a notice associated with the Produced Work reasonably calculated to make any Person that uses, views, accesses, interacts with, or is otherwise exposed to the Produced Work aware that Content was obtained from the Database, Derivative Database, or the Database as part of a Collective Database, and that it is available under this License. a. Example notice. The following text will satisfy notice under Section 4.3: Contains information from DATABASE NAME which is made available under the ODC Attribution License. DATABASE NAME should be replaced with the name of the Database and a hyperlink to the location of the Database. "ODC Attribution License" should contain a hyperlink to the URI of the text of this License. If hyperlinks are not possible, You should include the plain text of the required URI's with the above notice. 4.4 Licensing of others. You may not sublicense the Database. Each time You communicate the Database, the whole or Substantial part of the Contents, or any Derivative Database to anyone else in any way, the Licensor offers to the recipient a license to the Database on the same terms and conditions as this License. You are not responsible for enforcing compliance by third parties with this License, but You may enforce any rights that You have over a Derivative Database. You are solely responsible for any modifications of a Derivative Database made by You or another Person at Your direction. You may not impose any further restrictions on the exercise of the rights granted or affirmed under this License. ### 5.0 Moral rights 5.1 Moral rights. This section covers moral rights, including any rights to be identified as the author of the Database or to object to treatment that would otherwise prejudice the author's honour and reputation, or any other derogatory treatment: a. For jurisdictions allowing waiver of moral rights, Licensor waives all moral rights that Licensor may have in the Database to the fullest extent possible by the law of the relevant jurisdiction under Section 10.4; b. If waiver of moral rights under Section 5.1 a in the relevant jurisdiction is not possible, Licensor agrees not to assert any moral rights over the Database and waives all claims in moral rights to the fullest extent possible by the law of the relevant jurisdiction under Section 10.4; and c. For jurisdictions not allowing waiver or an agreement not to assert moral rights under Section 5.1 a and b, the author may retain their moral rights over certain aspects of the Database. Please note that some jurisdictions do not allow for the waiver of moral rights, and so moral rights may still subsist over the Database in some jurisdictions. ### 6.0 Fair dealing, Database exceptions, and other rights not affected 6.1 This License does not affect any rights that You or anyone else may independently have under any applicable law to make any use of this Database, including without limitation: a. Exceptions to the Database Right including: Extraction of Contents from non-electronic Databases for private purposes, Extraction for purposes of illustration for teaching or scientific research, and Extraction or Re-utilisation for public security or an administrative or judicial procedure. b. Fair dealing, fair use, or any other legally recognised limitation or exception to infringement of copyright or other applicable laws. 6.2 This License does not affect any rights of lawful users to Extract and Re-utilise insubstantial parts of the Contents, evaluated quantitatively or qualitatively, for any purposes whatsoever, including creating a Derivative Database (subject to other rights over the Contents, see Section 2.4). The repeated and systematic Extraction or Re-utilisation of insubstantial parts of the Contents may however amount to the Extraction or Re-utilisation of a Substantial part of the Contents. ### 7.0 Warranties and Disclaimer 7.1 The Database is licensed by the Licensor "as is" and without any warranty of any kind, either express, implied, or arising by statute, custom, course of dealing, or trade usage. Licensor specifically disclaims any and all implied warranties or conditions of title, non-infringement, accuracy or completeness, the presence or absence of errors, fitness for a particular purpose, merchantability, or otherwise. Some jurisdictions do not allow the exclusion of implied warranties, so this exclusion may not apply to You. ### 8.0 Limitation of liability 8.1 Subject to any liability that may not be excluded or limited by law, the Licensor is not liable for, and expressly excludes, all liability for loss or damage however and whenever caused to anyone by any use under this License, whether by You or by anyone else, and whether caused by any fault on the part of the Licensor or not. This exclusion of liability includes, but is not limited to, any special, incidental, consequential, punitive, or exemplary damages such as loss of revenue, data, anticipated profits, and lost business. This exclusion applies even if the Licensor has been advised of the possibility of such damages. 8.2 If liability may not be excluded by law, it is limited to actual and direct financial loss to the extent it is caused by proved negligence on the part of the Licensor. ### 9.0 Termination of Your rights under this License 9.1 Any breach by You of the terms and conditions of this License automatically terminates this License with immediate effect and without notice to You. For the avoidance of doubt, Persons who have received the Database, the whole or a Substantial part of the Contents, Derivative Databases, or the Database as part of a Collective Database from You under this License will not have their licenses terminated provided their use is in full compliance with this License or a license granted under Section 4.8 of this License. Sections 1, 2, 7, 8, 9 and 10 will survive any termination of this License. 9.2 If You are not in breach of the terms of this License, the Licensor will not terminate Your rights under it. 9.3 Unless terminated under Section 9.1, this License is granted to You for the duration of applicable rights in the Database. 9.4 Reinstatement of rights. If you cease any breach of the terms and conditions of this License, then your full rights under this License will be reinstated: a. Provisionally and subject to permanent termination until the 60th day after cessation of breach; b. Permanently on the 60th day after cessation of breach unless otherwise reasonably notified by the Licensor; or c. Permanently if reasonably notified by the Licensor of the violation, this is the first time You have received notice of violation of this License from the Licensor, and You cure the violation prior to 30 days after your receipt of the notice. 9.5 Notwithstanding the above, Licensor reserves the right to release the Database under different license terms or to stop distributing or making available the Database. Releasing the Database under different license terms or stopping the distribution of the Database will not withdraw this License (or any other license that has been, or is required to be, granted under the terms of this License), and this License will continue in full force and effect unless terminated as stated above. ### 10.0 General 10.1 If any provision of this License is held to be invalid or unenforceable, that must not affect the validity or enforceability of the remainder of the terms and conditions of this License and each remaining provision of this License shall be valid and enforced to the fullest extent permitted by law. 10.2 This License is the entire agreement between the parties with respect to the rights granted here over the Database. It replaces any earlier understandings, agreements or representations with respect to the Database. 10.3 If You are in breach of the terms of this License, You will not be entitled to rely on the terms of this License or to complain of any breach by the Licensor. 10.4 Choice of law. This License takes effect in and will be governed by the laws of the relevant jurisdiction in which the License terms are sought to be enforced. If the standard suite of rights granted under applicable copyright law and Database Rights in the relevant jurisdiction includes additional rights not granted under this License, these additional rights are granted in this License in order to meet the terms of this License.