Inferring Min and Max Invariants Using Max-Plus Polyhedra

DOI10.1007/978-3-540-69166-2_13zbMATH Open1149.68346OpenAlexW1499377964MaRDI QIDQ3522071FDOQ3522071

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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
• Inferring sufficient conditions with backward polyhedral under-approximations
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Model Checking Real-Time Systems
• Conditional reachability of uncertain max plus linear systems
• Approximating the volume of tropical polytopes is difficult
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• On just-in-time control of timed event graphs with input constraints: a semimodule approach
• 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)