Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

DOI10.1016/j.cl.2015.11.001zbMath1379.68239OpenAlexW2192877587MaRDI QIDQ681335

John P. Gallagher, Bishoksan Kafle

Publication date: 30 January 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2015.11.001

zbMATH Keywords

Horn clausesabstract interpretationfinite tree automatatree automata determinisation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

An iterative approach to precondition inference using constrained Horn clauses ⋮ Transformation-Enabled Precondition Inference ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Predicate Pairing for program verification ⋮ Tree dimension in verification of constrained Horn clauses

Uses Software

• SLAM
• ARMC
• Dagger
• PPL
• TRACER
• InvGen
• HSF
• SeaHorn
• VeriMAP

Cites Work

• Widening with Thresholds for Programs with Complex Control Graphs
• Refinement of Trace Abstraction
• Counterexample-guided abstraction refinement for symbolic model checking
• Nested interpolants
• Failure tabled constraint logic programming by interpolation
• Automatically Refining Abstract Interpretations
• Logic Programming
• Constraint-based deductive model checking

This page was built for publication: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement