The octagon abstract domain

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

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: Theory and Practice
• 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)

• Title not available (Why is that?)
• Incrementally closing octagons
• The octagon abstract domain for continuous constraints
• Sound Bit-Precise Numerical Domains
• Improving Strategies via SMT Solving
• A sparse evaluation technique for detailed semantic analyses
• Extracting Program Logics From Abstract Interpretations Defined by Logical Relations
• Quantitative static analysis of communication protocols using abstract Markov chains
• Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints
• Automation of Quantitative Information-Flow Analysis
• Numerical invariants through convex relaxation and max-strategy iteration
• Inferring Effective Types for Static Analysis of C Programs
• Access Analysis-Based Tight Localization of Abstract Memories
• Modelling declassification policies using abstract domain completeness
• 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
• Compact Difference Bound Matrices
• Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT
• Static Analysis of Communicating Processes Using Symbolic Transducers
• A flow-insensitive-complete program representation
• Relational string abstract domains
• Linear Absolute Value Relation Analysis
• 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
• Feasibility checking in Horn constraint systems through a reduction based approach
• Quadtrees as an abstract domain
• Speeding up the Constraint-Based Method in Difference Logic
• 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
• On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems
• Verifying constant-time implementations by abstract interpretation
• Access-Based Localization for Octagons
• Transfer Function Synthesis without Quantifier Elimination
• Predicate Pairing for program verification
• Abstract Interpretation with Applications to Timing Validation
• Generic Abstraction of Dictionaries and Arrays
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• The octatope abstract domain for verification of neural networks
• A Scalable Segmented Decision Tree Abstract Domain
• Narrowing Operators on Template Abstract Domains
• Proving Termination by Policy Iteration
• Fully Bounded Polyhedral Analysis of Integers with Wrapping
• Analyzing fractional Horn constraint systems
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Scalable polyhedral verification of recurrent neural networks
• Iterating Octagons
• Incremental closure for systems of two variables per inequality
• TreeKs: A Functor to Make Numerical Abstract Domains Scalable
• Inverse-limit and topological aspects of abstract interpretation
• Title not available (Why is that?)
• Symbolic Model Checking in Non-Boolean Domains
• 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
• Neighborhood persistency of the linear optimization relaxation of integer linear optimization
• From invariant checking to invariant inference using randomized search
• The Abstract Domain of Parallelotopes
• The abstract domain of trapezoid step functions
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• An iterative approach to precondition inference using constrained Horn clauses
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Discovering invariants via simple component analysis
• Building Certified Static Analysers by Modular Construction of Well-founded Lattices
• An extension of lazy abstraction with interpolation for programs with arrays
• 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
• Abstract interpretation from a denotational-semantics perspective
• Range and set abstraction using SAT
• An abstract domain to discover interval linear equalities
• Experimental evaluation of numerical domains for inferring ranges
• Finding Relevant Templates via the Principal Component Analysis
• Octagon
• An Iterative Method for Generating Loop Invariants
• Descending chains and narrowing on template abstract domains
• Automatically proving termination and memory safety for programs with pointer arithmetic
• The two variable per inequality abstract domain
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Constructive Galois Connections
• A new abstraction framework for affine transformers
• On regions and zones for event-clock automata
• Integration of verification methods for program systems
• The octahedron abstract domain
• The octagon 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)