The octagon abstract domain

From MaRDI portal

Publication:853733

Jump to:navigation, search

DOI10.1007/s10990-006-8609-1zbMath1105.68069OpenAlexW3158747708WikidataQ55970407 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

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

Related Items

Automation of Quantitative Information-Flow Analysis, Unnamed Item, Transformation-Enabled Precondition Inference, Relational abstract interpretation of arrays in assembly code, Symbolic analysis of linear hybrid automata -- 25 years later, Lifting numeric relational domains to algebraic data types, Invariant inference with provable complexity from the monotone theory, Neighborhood persistency of the linear optimization relaxation of integer linear optimization, A faster algorithm for determining the linear feasibility of systems of BTVPI constraints, The octatope abstract domain for verification of neural networks, Decoupling the ascending and descending phases in abstract interpretation, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, Sweeping in Abstract Interpretation, Inferring Effective Types for Static Analysis of C Programs, Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes, An Improved Tight Closure Algorithm for Integer Octagonal Constraints, Narrowing Operators on Template Abstract Domains, Transfer Function Synthesis without Quantifier Elimination, Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model, What You Lose is What You Leak: Information Leakage in Declassification Policies, Extracting Program Logics From Abstract Interpretations Defined by Logical Relations, Automatically proving termination and memory safety for programs with pointer arithmetic, A generic framework for heap and value analyses of object-oriented programming languages, Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting, A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor global fixed-priority scheduling, Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data, Experimental evaluation of numerical domains for inferring ranges, Scalable polyhedral verification of recurrent neural networks, Symbolic Model Checking in Non-Boolean Domains, Compact Difference Bound Matrices, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, Why does Astrée scale up?, Static analysis of ReLU neural networks with tropical polyhedra, The octagon abstract domain, Relational string abstract domains, A flow-insensitive-complete program representation, Sparsity preserving algorithms for octagons, An iterative approach to precondition inference using constrained Horn clauses, Verifying constant-time implementations by abstract interpretation, Three improvements to the top-down solver, Descending chains and narrowing on template abstract domains, Modular inference of subprogram contracts for safety checking, Constraint solving for interpolation, A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints, Interprocedural Reachability for Flat Integer Programs, Horn clauses as an intermediate representation for program analysis and transformation, Integer feasibility and refutations in UTVPI constraints using bit-scaling, Inverse-limit and topological aspects of abstract interpretation, Static Analysis of Communicating Processes Using Symbolic Transducers, Stabilizing Floating-Point Programs Using Provenance Analysis, Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT, Finding Relevant Templates via the Principal Component Analysis, Sound Bit-Precise Numerical Domains, Abstract Interpretation with Applications to Timing Validation, A certifying algorithm for lattice point feasibility in a system of UTVPI constraints, Acceleration of the abstract fixpoint computation in numerical program analysis, Discovering invariants via simple component analysis, Analyzing fractional Horn constraint systems, Splitting the Control Flow with Boolean Flags, Reachability analysis for timed automata using max-plus algebra, A combinatorial algorithm for Horn programs, The two variable per inequality abstract domain, Modular Constraint Solver Cooperation via Abstract Interpretation, An extension of lazy abstraction with interpolation for programs with arrays, Incremental closure for systems of two variables per inequality, On regions and zones for event-clock automata, Linear Absolute Value Relation Analysis, Improving Strategies via SMT Solving, Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, Data flow analysis of asynchronous systems using infinite abstract domains, Abstract neural networks, Counterexample- and simulation-guided floating-point loop invariant synthesis, An Iterative Method for Generating Loop Invariants, Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints, Predicate Pairing for program verification, 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, An array content static analysis based on non-contiguous partitions, The abstract domain of trapezoid step functions, From invariant checking to invariant inference using randomized search, Numerical invariants through convex relaxation and max-strategy iteration, A combinatorial certifying algorithm for linear feasibility in UTVPI constraints, The Abstract Domain of Parallelotopes, Access-Based Localization for Octagons, TreeKs: A Functor to Make Numerical Abstract Domains Scalable, Generic Abstraction of Dictionaries and Arrays, Proving Termination by Policy Iteration, Fully Bounded Polyhedral Analysis of Integers with Wrapping, A Scalable Segmented Decision Tree Abstract Domain, Widening and narrowing operators for abstract interpretation, On integer closure in a system of unit two variable per inequality constraints, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses, Inferring functional properties of matrix manipulating programs by abstract interpretation, Static Contract Checking with Abstract Interpretation, Iterating Octagons, An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints, Abstract Interpretation From a Denotational-semantics Perspective, Access Analysis-Based Tight Localization of Abstract Memories, A decision tree lifted domain for analyzing program families with numerical features, On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems, Range and Set Abstraction using SAT, Relational Abstract Domain of Weighted Hexagons, Quadtrees as an Abstract Domain, A Note on the Inversion Join for Polyhedral Analysis, Completeness of string analysis for dynamic languages, Constructive Galois Connections, Speeding up the Constraint-Based Method in Difference Logic, A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints, Octagon, Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships, Logahedra: A New Weakly Relational Domain, Modelling declassification policies using abstract domain completeness, Quantitative static analysis of communication protocols using abstract Markov chains, A new abstraction framework for affine transformers, Integration of verification methods for program systems, Incrementally closing octagons, A sparse evaluation technique for detailed semantic analyses, The octagon abstract domain for continuous constraints, Feasibility checking in Horn constraint systems through a reduction based approach

Uses Software

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:853733&oldid=12797606"