Tree dimension in verification of constrained Horn clauses

DOI10.1017/S1471068418000030zbMath1478.68165arXiv1803.01448OpenAlexW2964124669WikidataQ129837133 ScholiaQ129837133MaRDI QIDQ4644355

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

Horn clausesspecificationtree dimensionanalysis and verification of systems

Mathematics Subject Classification ID

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

Related Items (3)

Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Yices
• PPL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• Newtonian program analysis via tensor product
• Generalized Property Directed Reachability
• An overview of Ciao and its design philosophy
• Horn Clause Solvers for Program Verification
• Newtonian program analysis
• Refinement of Trace Abstraction
• On Fixed Point Equations over Commutative Semirings
• Combining Widening and Acceleration in Linear Relation Analysis
• The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Synchronizing Constrained Horn Clauses
• A Brief History of Strahler Numbers

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