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

DOI10.1016/J.CL.2015.11.001MaRDI QIDQ681335zbMATH OpenOpenAlexFDO

Authors Bishoksan Kafle, John P. Gallagher

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

abstract interpretationHorn clausesfinite tree automatatree automata determinisation

Mathematics Subject Classification ID

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

Recommendations

• Tree automata-based refinement with application to Horn clause verification
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
• Horn clause solvers for program verification
• Automating induction for solving Horn clauses
• Tree dimension in verification of constrained Horn clauses

Cites work

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

Cited in

(10)

• Inferring simple solutions to recursion-free Horn clauses via sampling
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Predicate pairing for program verification
• scientific article; zbMATH DE number 7214004 (Why is no real title available?)
• An iterative approach to precondition inference using constrained Horn clauses
• Tree automata-based refinement with application to Horn clause verification
• Transformation-Enabled Precondition Inference
• Solving non-linear Horn clauses using a linear Horn clause solver
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
• Tree dimension in verification of constrained Horn clauses

Describes a project that uses

Uses Software

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

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

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