Two variables per linear inequality as an abstract domain

DOI10.1007/3-540-45013-0_7MaRDI QIDQ3079912zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(29)

• Incremental closure for systems of two variables per inequality
• Generic abstraction of dictionaries and arrays
• Completeness of string analysis for dynamic languages
• Linear absolute value relation analysis
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Narrowing operators on template abstract domains
• 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
• Experimental evaluation of numerical domains for inferring ranges
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• Static contract checking with abstract interpretation
• 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
• Analyzing fractional Horn constraint systems
• Generalizing the template polyhedral domain

Describes a project that uses

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)