Combining Forward and Backward Abstract Interpretation of Horn Clauses

DOI10.1007/978-3-319-66706-5_2zbMath1420.68062arXiv1707.01277OpenAlexW2729908430MaRDI QIDQ5233235

David Monniaux, Alexey Bakhirkin

Publication date: 16 September 2019

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1707.01277

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

On the copy complexity of width 3 Horn constraint systems ⋮ Analyzing read-once cutting plane proofs in Horn systems ⋮ Transformation-Enabled Precondition Inference ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Analyzing fractional Horn constraint systems ⋮ Copy complexity of Horn formulas with respect to unit read-once resolution ⋮ On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations

This page was built for publication: Combining Forward and Backward Abstract Interpretation of Horn Clauses