Incremental closure for systems of two variables per inequality

DOI10.1016/J.TCS.2018.12.001MaRDI QIDQ1733055zbMATH OpenOpenAlexFDO

Authors Jacob M. Howe, Andy King, Axel Simon

Publication date 26 March 2019

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

Copyright license Creative Commons Attribution 4.0 International

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

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

Recommendations

• On integer closure in a system of unit two variable per inequality constraints
• The two variable per inequality abstract domain
• Incremental satisfiability and implication for UTVPI constraints
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints

Cites work

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

Cited in

(4)

• On integer closure in a system of unit two variable per inequality constraints
• Two variables per linear inequality as an abstract domain
• The two variable per inequality abstract domain
• Canonical forms and widening for two variables per inequality systems

Describes a project that uses

Uses Software

• Algorithm 97
• Apron

This page was built for publication: Incremental closure for systems of two variables per inequality

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