Tree dimension in verification of constrained Horn clauses

DOI10.1017/S1471068418000030zbMath1478.68165arXiv1803.01448MaRDI 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 clauses; specification; tree dimension; analysis and verification of systems

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

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