Abstract Interpretation Frameworks

By P. Cousot, R. Cousot. 1992

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, background): “, [6], [7]), a theory which dictates how to obtain sound, computable, and precise finite approximations of potentially infinite sets of behaviors.”
A static analyzer for large safety-critical software (2003, background): “, E ] n+1 = E n a F (E n) where the narrowing operator a is sound (the concretization of x a y is an upper approximation of the intersection of x and y) and ensures termination [8, 11].”
Model checking programs (2000, background): “Recently, the use of abstraction algorithms based on the theory of abstract interpretation [8], have received much attention in the model checking community [14, 9, 36, 37, 5].”
Opacity generalised to transition systems (2005, methodology): “As initial opacity is, in general, undecidable when labelled transition systems are allowed to be infinite, we propose in this section a technique which might allow to verify it, at least in some cases, using a technique close to abstract interpretation [7,8].”
The octagon abstract domain (2001, methodology): “In this paper, we will work in the Abstract Interpretation framework [18, 20 ] which is a general theory of the approximation of program semantics.”
AI 2 : Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, background): “, [2], [3]), a theory which dictates how to obtain sound, computable, and precise finite approximations of potentially infinite sets of behaviors.”
The ASTREÉ Analyzer (2005, background): “It follows that the abstract fixpoint transformer is non-monotonic, which is not an issue as it abstracts monotonic concrete fixpoints [6].”
Contracts for System Design (2018, background): “A known formalization of this is the notion of Galois connection, which is key in the theory of Abstract Interpretation [92, 93, 94, 202].”
The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems (2006, methodology): “For this reason, the domains can be so employed only in conjunction with appropriate mechanisms for enforcing and/or accelerating the convergence of ﬁxpoint computations: widening operators [30,31,33,34] provide a simple and general characterization for such mechanisms.”