Inferring Min and Max Invariants Using Max-Plus Polyhedra

DOI10.1007/978-3-540-69166-2_13MaRDI QIDQ3522071zbMATH OpenOpenAlexFDO

Authors Xavier Allamigeon, Stéphane Gaubert, Éric Goubault

Publication date 28 August 2008

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69166-2_13

Mathematics Subject Classification ID

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

Recommendations

• Abstract interpretation meets convex optimization
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• The octagon abstract domain
• Fast polyhedra abstract domain

Cites work

• scientific article; zbMATH DE number 3869093 (Why is no real title available?)
• scientific article; zbMATH DE number 3570223 (Why is no real title available?)
• scientific article; zbMATH DE number 627763 (Why is no real title available?)
• scientific article; zbMATH DE number 2221682 (Why is no real title available?)
• A framework for numeric analysis of array operations
• Affine relationships among variables of a program
• Algorithm for discovering the set of all the solutions of a linear programming problem
• Duality and separation theorems in idempotent semimodules.
• Generators, extremals and bases of max cones
• Idempotent functional analysis: An algebraic approach
• Max-Plus Convex Geometry
• Methods and applications of \((\max,+)\) linear algebra
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Programming Languages and Systems
• Static Analysis in Disjunctive Numerical Domains
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Sufficient Preconditions for Modular Assertion Checking
• The Minkowski theorem for max-plus convex sets
• The duality theorem for min-max functions
• Tropical convexity
• Tropical halfspaces
• Verification, Model Checking, and Abstract Interpretation

Cited in

(21)

• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• On the complexity of strongly connected components in directed hypergraphs
• Tropical linear-fractional programming and parametric mean payoff games
• Donut domains: efficient non-convex domains for abstract interpretation
• On the control of max-plus linear system subject to state restriction
• The tropical analogue of polar cones
• Linear absolute value relation analysis
• Block-wise abstract interpretation by combining abstract domains with SMT
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• The number of extreme points of tropical polyhedra
• Reachability analysis for timed automata using max-plus algebra
• Static analysis of ReLU neural networks with tropical polyhedra
• Computing the vertices of tropical polyhedra using directed hypergraphs
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Inferring sufficient conditions with backward polyhedral under-approximations
• Model Checking Real-Time Systems
• Conditional reachability of uncertain max plus linear systems
• Approximating the volume of tropical polytopes is difficult
• On just-in-time control of timed event graphs with input constraints: a semimodule approach
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis

This page was built for publication: Inferring Min and Max Invariants Using Max-Plus Polyhedra

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