INTERPRETATION : ‘A UNIFIED LATTICE MODEL FOR STATIC ANALYSIS OF PROGRAMS BY CONSTRUCTION OR APPROXIMATION

By P. Cousot, R. Cousot

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): “The AI(2) system is fully integrated with all abstract domains supported by Apron [20], a popular library for numerical abstract domains, including: Box [7], Zonotope [10], and Polyhedra [8].”
Language-based information-flow security (2003, methodology): “The framework ofabstract interpretation[133] is a powerful methodology for designing static analyses that are sound by construction.”
Static Analysis in Disjunctive Numerical Domains (2006, methodology): “Abstract interpretation [7] is a generic technique for computing inductive assertions of CFGs using an iterative process.”
The Zonotope Abstract Domain Taylor1+ (2009, background): “Fixpoint computation using Kleene-like iteration For both filters, we detail results for two different (i, c,N )-iteration schemes (see end of Section 2.2) for Taylor1+, with i = 0 and N = 103.”
Software model checking (2009, unknown): “In abstract model checking, reachability analysis is performed on an abstract domain which captures some, but not necessarily all, the information about an execution, using an abstract semantics of the program [Cousot and Cousot 1977].”
Boolean and Cartesian abstraction for model checking C programs (2001, methodology): “‘Loss of precision’ is made formally precise in the following way (see [ 8 ,12]).”
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].”
Linear Invariant Generation Using Non-linear Constraint Solving (2003, background): “The dominant invariant generation technique is abstract interpretation [6].”
A Software Analysis Perspective (2012, methodology): “The Value plugin (short for Value Analysis) is a forward dataflow analysis based on the principles of abstract interpretation [17].”
MaxSMT-Based Type Inference for Python 3 (2018, background): “Pytype infers PEP484 [25] gradual type annotations by abstract interpretation [5] of the bytecode-compiled version of the given Python file.”
Extended static checking for Java (2002, methodology): “Abstract interpretation [6] is a more established technique; it uses heuristics to iteratively build up an abstract model of a program.”
Non-linear loop invariant generation using Gröbner bases (2004, unknown): “Categories and Subject Descriptors: F.3.1 [Verifying Programs]: Invariants, I.1.2 [Algorithms]:Algebraic Algorithms, F.4.1 [Mathematical Logic]:Logic and Constraint Programming, F.3.2 [Semantics of Programming]: Program Analysis.”
Maximum Resilience of Artificial Neural Networks (2017, methodology): “We apply static analysis [7] based on interval arithmetic for propagating the bounded input values”
Abstract Interpretation Frameworks (1992, methodology): “Then, the abstract interpretation focuses on a class of properties of program execu tions, which is usually defined by a collecting semantics (also called static in [7]).”
Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, methodology): “• Abstract interpretation methods: Abstract interpretation is a theory of approximation of mathematical structures, in particular those that arise in defining the semantic models of computer systems (Cousot and Cousot (1977)).”
Deductive Software Verification – The KeY Book (2016, methodology): “It is connected to D with an abstraction function α : 2D→ A and a concretization function γ : A→ 2D which form a Galois insertion [Cousot and Cousot, 1977], i.”
CacheAudit: A Tool for the Static Analysis of Cache Side Channels (2013, methodology): “This set can be overapproximated by abstract interpretation, which is a theory of sound approximation of program semantics [Cousot and Cousot 1977], and its cardinality can be determined by counting techniques [K ¨ opf and Rybalchenko 2010].”