Tree dimension in verification of constrained Horn clauses

DOI10.1017/S1471068418000030MaRDI QIDQ4644355zbMATH OpenOpenAlexWikidataFDO

Authors Bishoksan Kafle, John P. Gallagher, Pierre Ganty

Publication date 31 May 2018

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

specificationHorn clausestree dimensionanalysis and verification of systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCs $P$, we define a transformation of $P$ yielding a dimension bounded set of CHCs $P^{leqk}$. The set of derivations for $P^{leqk}$ consists of the derivations for $P$ that have dimension at most $k$. We also show how to construct a set of clauses denoted $P^{>k}$ whose derivations have dimension exceeding $k$. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).

Recommendations

• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• Tree automata-based refinement with application to Horn clause verification
• Solving non-linear Horn clauses using a linear Horn clause solver
• Solving Horn clauses on inductive data types without induction
• scientific article; zbMATH DE number 7444022

Cites work

• scientific article; zbMATH DE number 108368 (Why is no real title available?)
• scientific article; zbMATH DE number 1178950 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• A Brief History of Strahler Numbers
• An overview of Ciao and its design philosophy
• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• Combining Widening and Acceleration in Linear Relation Analysis
• Generalized property directed reachability
• Horn clause solvers for program verification
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• Newtonian program analysis
• Newtonian program analysis via tensor product
• On Fixed Point Equations over Commutative Semirings
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Refinement of Trace Abstraction
• Solving non-linear Horn clauses using a linear Horn clause solver
• Synchronizing constrained Horn clauses
• The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1

Cited in

(7)

• Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• scientific article; zbMATH DE number 7453192 (Why is no real title available?)
• Tree automata-based refinement with application to Horn clause verification
• scientific article; zbMATH DE number 7453190 (Why is no real title available?)
• Deciding validity in a spatial logic for trees
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

Describes a project that uses

Uses Software

• PPL
• Yices

This page was built for publication: Tree dimension in verification of constrained Horn clauses

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