Scientific publications

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

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

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

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