1,720,993 research outputs found
On the interaction between sharing and linearity
No full textIn the analysis of logic programs, abstract domains for detecting sharing and linearity information are widely used. Devising abstract unification algorithms for such domains has proved to be rather hard. At the moment, the available algorithms are correct but not optimal; i.e., they cannot fully exploit the information conveyed by the abstract domains. In this paper, we define a new (infinite) domain ShLinω which can be thought of as a general framework from which other domains can be easily derived by abstraction. ShLinω makes the interaction between sharing and linearity explicit. We provide a constructive characterization of the optimal abstract unification operator on ShLinω, and we lift it to two well-known abstractions of ShLinω, namely, to the classical Sharing × Lin abstract domain and to the more precise ShLin2 abstract domain by Andy King. In the case of single-binding substitutions, we obtain optimal abstract unification algorithms for such domains
Optimality in goal-dependent Analysis of Sharing
No full textWe cope with the problem of correctness and optimality for logic
programs analysis by abstract interpretation. We refine the
goal-dependent framework appeared in [CF99] by fixing a result
of correctness and introducing two specialized operators for forward
and backward unification. We provide the best correct abstractions
of the concrete operators in the case of set-sharing analysis. We
show that the precision of the overall analysis is strictly improved
and that, in some cases, we gain precision w.r.t. more complex
domains involving linearity and freeness information
Random: R-based Analyzer for Numerical Domains
No full textRandom is a static analyzer of programs, based on the theory of abstract interpretation. It can analyze simple imperative R programs (with the standard constructs while, for, if-then-else) with 4 abstract domains: intervals, template parallelotopes, a combination of intervals and template parallelotopes and, finally, general (non-template) parallelotopes
Analysis and Verification of Navigation Strategies by Abstract Interpretation of Cellular Automata
No full textWe present a new approach to the analysis and verification of simple properties of character navigation. We model navigation strategies for virtual characters by cellular automata, and use standard abstract interpretation techniques for abstracting and verifying navigation properties
A General Framework for Variable Aliasing: Towards Optimal Operators for Sharing Properties
No full textJGMP: Java bindings and wrappers for the GMP library
Get PDFThe GNU Multiple Precision Arithmetic Library (GMP) is a widely used library for computing with arbitrary precision arithmetic. The library has functionally complete bindings for many programming languages, including .NET, C++, OCaml, Python, Ruby, and Rust, with the notable exception of Java. The JGMP library provides Java bindings and wrappers for using GMP from within any JVM-based language. The library has been thoroughly tested and benchmarked
Localizing Widening and Narrowing
No full textWe show two strategies which may be easily applied to standard abstract interpretation-based static analyzers. They consist in 1) restricting the scope of widening, and 2) intertwining the computation of ascending and descending chains. Using these optimizations it is possible to improve the precision of the analysis, without any change to the abstract domains
- …
