Incremental closure for systems of two variables per inequality

DOI10.1016/j.tcs.2018.12.001zbMath1417.68103OpenAlexW2902161729MaRDI QIDQ1733055

Jacob M. Howe, Axel Simon, Andy King

Publication date: 26 March 2019

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2018.12.001

zbMATH Keywords

abstract interpretationtwo variables per inequality (TVPI) abstract domainweakly relational abstract domains

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Linear programming (90C05) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Apron
• Algorithm 97

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Some efficient solutions to the affine scheduling problem. I: One- dimensional time
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• The octagon abstract domain
• The octahedron abstract domain
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Dataflow analysis of array and scalar references
• Monotonizing linear programs with up to two nonzeroes per column
• Exploiting sparsity in difference-bound matrices
• A polynomial combinatorial algorithm for generalized minimum cost flow
• Incremental Satisfiability and Implication for UTVPI Constraints
• Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra
• Two Variables per Linear Inequality as an Abstract Domain
• On a routing problem
• Taming the Wrapping of Integer Arithmetic
• Logahedra: A New Weakly Relational Domain
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with Two Variables Per Inequality
• Efficient Algorithms for Shortest Paths in Sparse Networks
• On proof and progress in mathematics
• Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality
• Improved Algorithms For Linear Inequalities with Two Variables Per Inequality
• Static Analysis
• Frontiers of Combining Systems
• The Organization of Computations for Uniform Recurrence Equations
• A Theorem on Boolean Matrices