Two variables per linear inequality as an abstract domain

DOI10.1007/3-540-45013-0_7zbMATH Open1278.68072OpenAlexW1957766372MaRDI QIDQ3079912FDOQ3079912

Authors: Axel Simon, Andy King, Jacob M. Howe 

Publication date: 4 March 2011

Published in: Logic Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: http://openaccess.city.ac.uk/1709/1/Two_variables_per_linear_inequality_as_an_abstract_domain.pdf

Recommendations

• The two variable per inequality abstract domain
• Incremental closure for systems of two variables per inequality
• An abstract domain to discover interval linear equalities
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• scientific article; zbMATH DE number 1738295

Mathematics Subject Classification ID

Computational aspects related to convexity (52B55) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (29)

• Incremental closure for systems of two variables per inequality
• Generic abstraction of dictionaries and arrays
• Linear absolute value relation analysis
• Completeness of string analysis for dynamic languages
• Narrowing operators on template abstract domains
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• On the efficiency of convex polyhedra
• Discovering invariants via simple component analysis
• On integer closure in a system of unit two variable per inequality constraints
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Splitting the Control Flow with Boolean Flags
• A combinatorial algorithm for Horn programs
• A note on the inversion join for polyhedral analysis
• Range and set abstraction using SAT
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• Static contract checking with abstract interpretation
• Experimental evaluation of numerical domains for inferring ranges
• On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
• Quadtrees as an abstract domain
• Descending chains and narrowing on template abstract domains
• Exact join detection for convex polyhedra and other numerical abstractions
• The two variable per inequality abstract domain
• Sweeping in Abstract Interpretation
• The octagon abstract domain
• Relational abstract domain of weighted hexagons
• Logahedra: a new weakly relational domain
• Clustered relational thread-modular abstract interpretation with local traces
• Generalizing the template polyhedral domain
• Analyzing fractional Horn constraint systems

Uses Software

• Octagon

This page was built for publication: Two variables per linear inequality as an abstract domain

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