Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations

DOI10.1016/j.entcs.2012.09.009zbMath1294.68062OpenAlexW4310979390WikidataQ113318056 ScholiaQ113318056MaRDI QIDQ5170174

Antoine Miné

Publication date: 22 July 2014

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.09.009

zbMATH Keywords

polyhedrastatic analysisabstract interpretationbackward analysis

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Efficient constraint/generator removal from double description of polyhedra ⋮ An iterative approach to precondition inference using constrained Horn clauses ⋮ Transformation-Enabled Precondition Inference ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation

Uses Software

• Apron
• ESC/Java

Cites Work

• An abstract interpretation framework for termination
• Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
• Guarded commands, nondeterminacy and formal derivation of programs
• Sufficient Preconditions for Modular Assertion Checking
• Static Analysis
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation