The octagon abstract domain

DOI10.1007/S10990-006-8609-1zbMATH Open1105.68069DBLPjournals/lisp/Mine06OpenAlexW3158747708WikidataQ55970407 ScholiaQ55970407MaRDI QIDQ853733FDOQ853733

Authors: Antoine Miné 

Publication date: 17 November 2006

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-006-8609-1

Recommendations

• Incrementally closing octagons
• Static Analysis
• The octahedron abstract domain
• Compact Difference Bound Matrices
• The octagon abstract domain for continuous constraints

zbMATH Keywords

Abstract interpretationStatic analysisNumerical abstract domainsRelational numerical invariants

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• Title not available (Why is that?)
• The octagon abstract domain
• Title not available (Why is that?)
• On a routing problem
• Title not available (Why is that?)
• Affine relationships among variables of a program
• Abstract interpretation and application to logic programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Two variables per linear inequality as an abstract domain
• Static analysis of arithmetical congruences
• Title not available (Why is that?)
• Title not available (Why is that?)
• Abstract Interpretation Frameworks
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Verification by abstract interpretation
• Static Analysis
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Programming Languages and Systems
• Static Analysis
• Abstract interpretation of mobile systems

Cited In (only showing first 100 items - show all)

• Incremental closure for systems of two variables per inequality
• Donut domains: efficient non-convex domains for abstract interpretation
• Title not available (Why is that?)
• Incrementally closing octagons
• Generic abstraction of dictionaries and arrays
• The octagon abstract domain for continuous constraints
• A sparse evaluation technique for detailed semantic analyses
• Predicate pairing for program verification
• Linear absolute value relation analysis
• Proving termination by policy iteration
• Quantitative static analysis of communication protocols using abstract Markov chains
• Narrowing operators on template abstract domains
• Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints
• Numerical invariants through convex relaxation and max-strategy iteration
• Static analysis of communicating processes using symbolic transducers
• Block-wise abstract interpretation by combining abstract domains with SMT
• Neighborhood persistency of the linear optimization relaxation of integer linear optimization
• The abstract domain of trapezoid step functions
• Speeding up the constraint-based method in difference logic
• On integer closure in a system of unit two variable per inequality constraints
• Stabilizing Floating-Point Programs Using Provenance Analysis
• A note on the inversion join for polyhedral analysis
• Static analysis of ReLU neural networks with tropical polyhedra
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• A scalable segmented decision tree abstract domain
• Compact Difference Bound Matrices
• A flow-insensitive-complete program representation
• Relational string abstract domains
• A decision tree lifted domain for analyzing program families with numerical features
• Abstract neural networks
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints
• An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints
• A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
• Automation of quantitative information-flow analysis
• On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
• Feasibility checking in Horn constraint systems through a reduction based approach
• Quadtrees as an abstract domain
• Inferring functional properties of matrix manipulating programs by abstract interpretation
• Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses
• Verifying constant-time implementations by abstract interpretation
• The abstract domain of parallelotopes
• Inferring effective types for static analysis of C programs
• Transfer function synthesis without quantifier elimination
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• The octatope abstract domain for verification of neural networks
• Improving strategies via SMT solving
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• Fully Bounded Polyhedral Analysis of Integers with Wrapping
• Sound bit-precise numerical domains
• Analyzing fractional Horn constraint systems
• Access analysis-based tight localization of abstract memories
• Access-based localization for octagons
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Constructive Galois connections
• Scalable polyhedral verification of recurrent neural networks
• Iterating Octagons
• Inverse-limit and topological aspects of abstract interpretation
• Title not available (Why is that?)
• A zonotopic framework for functional abstractions
• A generic framework for heap and value analyses of object-oriented programming languages
• A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor global fixed-priority scheduling
• Completeness of string analysis for dynamic languages
• Lifting numeric relational domains to algebraic data types
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• From invariant checking to invariant inference using randomized search
• An iterative method for generating loop invariants
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• An iterative approach to precondition inference using constrained Horn clauses
• Finding relevant templates via the principal component analysis
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Discovering invariants via simple component analysis
• An extension of lazy abstraction with interpolation for programs with arrays
• An abstract domain of uninterpreted functions
• Verification, Model Checking, and Abstract Interpretation
• Reachability analysis for timed automata using max-plus algebra
• Widening and narrowing operators for abstract interpretation
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Splitting the Control Flow with Boolean Flags
• A combinatorial algorithm for Horn programs
• Constraint solving for interpolation
• Modular inference of subprogram contracts for safety checking
• Static Analysis
• Sparsity preserving algorithms for octagons
• Static analysis of binary code with memory indirections using polyhedra
• Abstract interpretation from a denotational-semantics perspective
• Range and set abstraction using SAT
• Static analysis of run-time errors in embedded critical parallel C programs
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• An abstract domain to discover interval linear equalities
• Simple and efficient algorithms for octagons
• Static contract checking with abstract interpretation
• Experimental evaluation of numerical domains for inferring ranges
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Octagon
• Descending chains and narrowing on template abstract domains
• Building certified static analysers by modular construction of well-founded lattices
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Interprocedural reachability for flat integer programs
• The two variable per inequality abstract domain

Uses Software

• Apron
• ASTREE

This page was built for publication: The octagon abstract domain

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q853733)