The octagon abstract domain

DOI10.1007/s10990-006-8609-1zbMath1105.68069WikidataQ55970407 ScholiaQ55970407MaRDI QIDQ853733

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

zbMATH Keywords

Static analysis; Abstract interpretation; Numerical abstract domains; Relational numerical invariants

Mathematics Subject Classification ID

68Q55: Semantics in the theory of computing

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes, An Improved Tight Closure Algorithm for Integer Octagonal Constraints, Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model, Transfer Function Synthesis without Quantifier Elimination, Octagon, Inverse-limit and topological aspects of abstract interpretation, Acceleration of the abstract fixpoint computation in numerical program analysis, Discovering invariants via simple component analysis, Reachability analysis for timed automata using max-plus algebra, Modular inference of subprogram contracts for safety checking, Constraint solving for interpolation, The two variable per inequality abstract domain, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, Why does Astrée scale up?, The octagon abstract domain, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Integration of verification methods for program systems, Widening and narrowing operators for abstract interpretation, Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data, Linear Absolute Value Relation Analysis, Improving Strategies via SMT Solving, Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, An Iterative Method for Generating Loop Invariants, Static Contract Checking with Abstract Interpretation, Access Analysis-Based Tight Localization of Abstract Memories, Modelling declassification policies using abstract domain completeness, Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships, Abstract Interpretation with Applications to Timing Validation, Splitting the Control Flow with Boolean Flags, A Scalable Segmented Decision Tree Abstract Domain, Iterating Octagons, Logahedra: A New Weakly Relational Domain

Uses Software

• Apron
• ASTREE

Cites Work

• The octagon abstract domain
• Affine relationships among variables of a program
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• Abstract interpretation of mobile systems
• Two Variables per Linear Inequality as an Abstract Domain
• On a routing problem
• Abstract interpretation and application to logic programs
• Static analysis of arithmetical congruences
• Abstract Interpretation Frameworks
• Verification: Theory and Practice
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item