Automatic discovery of linear restraints among variables of a program

By Patrick Cousot, Nicolas Halbwachs. 1978

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): “Polyhedra is a more precise domain than Zonotope: for our example, C includes only 5 integer points.”
A Logical Product Approach to Zonotope Intersection (2010, background): “The main reason for this is that the interpretation of linear assignments is exact and done in linear time in terms of the “complexity” of the zonotopes, and non-linear expressions are dynamically linearized in a rather inexpensive way, unlike for most of other sub-polyhedric domains (zones [19], li”
Abstract Interpretation Frameworks (1992, background): “In [17] , η would be the operator used at paragraph 3.”
Inferring Disjunctive Postconditions (2006, methodology): “For example, numerical invariants can be discovered by using numerical abstract domains like the interval domain [6] or the polyhedron domain [9].”
AI 2 : Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, background): “c) Polyhedra Domain [4]: The polyhedra domain consists of abstract elements that represent a convex polyhedron and are in turn represented as a set of linear constraints over the input variables.”
Fast polyhedra abstract domain (2017, background): “Examples of useful program properties involve the program’s heap [22, 26], numerical values [6, 14, 16, 17, 19, 30], termination [27, 28], and many others.”
A static analyzer for large safety-critical software (2003, background): “Even with this reduced cost, the huge number of live variables prevents us from representing sets of concrete environments as one big abstract state (as it was done for polyhedra in [13]).”
Predicate abstraction for software verification (2002, methodology): “Abstract interpretation [CC77] introduced the widening operator, which was used to compute [CH78] fixpoints more systematically.”
SPEED: precise and efficient static estimation of program computational complexity (2009, methodology): “We can use this methodology to combine an abstract interpreter for linear arithmetic (such as the one based on polyhedron domain [7]) with an abstract interpreter for uninterpreted functions [15].”
Linear Invariant Generation Using Non-linear Constraint Solving (2003, methodology): “After converting this into DNF and eliminating unsatisfiable disjuncts, we obtain the following generators shown along with the corresponding invariants: c1 c2 d c1i+ c2j + d ≤ 0 0 0 −1 −1 ≤ 0 0 −1 0 −j ≤ 0 −1 2 2 −i+ 2j + 2 ≤ 0 These match the invariants obtained in [7].”
Non-linear loop invariant generation using Gröbner bases (2004, methodology): “This technique has been applied with numerous refinements to generate invariants, especially linear invariants [18, 11 , 15, 6, 26, 5, 4]. However, apart from a few exceptions [3, 22], there has been little progress on the generation of non-linear invariants involving multiplication.”
Synthesis of interface specifications for Java classes (2005, methodology): “Abstract interpretation has been used to automatically generate invariants such as linear constraints over program variables [15, 23].”
The octagon abstract domain (2001, methodology): “Our analyzer is very similar to the one described in Cousot and Halbwachs’s POPL’78 article [6], except it uses our new abstract domain instead of the abstract domain of polyhedra .”
Apron: A Library of Numerical Abstract Domains for Static Analysis (2009, methodology): “In the past 30 years, many numerical abstract domains [6, 20, 21, 7, 10, 12, 13, 17] have been proposed, each defining a representation for a set of properties of interest and algorithms to manipulate them.”
An abstract domain for certifying neural networks (2019, background): “Our domain is less expressive than the Polyhedra domain [Cousot and Halbwachs 1978] because it bounds the number of conjuncts that can appear in the overall formula to 2 n where n is the number of variables of the network.”