🔬 Abstract Interpretation

Started by interval_catgirl · intervals numerical practical
The interval domain does not track relationships between variables, making it a non-relational domain.  When is that okay? Share your benchmarks and horror stories here.

Started by convex_nyaa · octagons polyhedra relational benchmarks
Examples of relational numerical abstract domains include octagons and convex polyhedra. When choosing an abstract domain, one typically has to strike a balance between keeping fine-grained relationships and high computational costs. Debate: which should you reach for first?

Started by lattice_purrfect · galois insertions
A Galois insertion is very similar to a Galois connection, but the abstract domain does not contain multiple elements that describe the same concrete values — no superfluous elements. Does it matter in practice? Discuss.

Started by omega_cat · infinite-domains widening
The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices (or lattices satisfying the chain condition).

Started by safety_neko · history safety-critical ariane5
The first large-scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996. A deep dive into how AI became critical for embedded systems verification.

Started by product_paw · reduced-product cartesian combination
The reduced product is a very important operator for combining abstract domains. Pair-widening and pair-narrowing operators can be combined when considering the cartesian product of two posets.

Started by fixpoint_femboy · semantics model-checking collecting
In Abstract Interpretation, the collecting semantics of a program is expressed as a least fix-point of a set of equations. The equations are solved over some abstract domain that captures the property of interest. Typically, the equations are solved iteratively until a fix-point is reached.

Started by nyatype_theorist · soundness completeness false-positives
Sometimes a loss of precision is necessary to make the semantics decidable. In general, there is a compromise to be made between the precision of the analysis and its decidability, or tractability. How do you cope? Vent here.