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)

• 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
• Logahedra: A New Weakly Relational Domain
• 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
• Experimental evaluation of numerical domains for inferring ranges
• Finding Relevant Templates via the Principal Component Analysis
• Octagon
• An Iterative Method for Generating Loop Invariants
• 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
• 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 octagon abstract domain
• Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
• Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
• Static Contract Checking with Abstract Interpretation
• Why does Astrée scale up?
• Relational abstract domain of weighted hexagons
• Data flow analysis of asynchronous systems using infinite abstract domains
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• Interprocedural Reachability for Flat Integer Programs
• Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting
• Horn clauses as an intermediate representation for program analysis and transformation
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• An array content static analysis based on non-contiguous partitions
• Automatic synthesis of \(k\)-inductive piecewise quadratic invariants for switched affine control programs
• Effective abstractions for verification under relaxed memory models
• Inference of ranking functions for proving temporal properties by abstract interpretation
• A combinatorial certifying algorithm for linear feasibility in UTVPI constraints
• Title not available (Why is that?)
• Incrementally closing octagons
• The octagon abstract domain for continuous constraints
• Modular Constraint Solver Cooperation via Abstract Interpretation
• 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
• Closing the performance gap between doubles and rationals for octagons
• 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
• A faster algorithm for determining the linear feasibility of systems of BTVPI constraints
• Stabilizing Floating-Point Programs Using Provenance Analysis
• Parameterized and exact-exponential algorithms for the read-once integer refutation problem in UTVPI constraints
• Decoupling the ascending and descending phases in abstract interpretation
• 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
• Transformation-Enabled Precondition Inference
• Logics for extensional, locally complete analysis via domain refinements
• Constrained read-once refutations in UTVPI constraint systems: a parallel perspective
• 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

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)