Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
From MaRDI portal
Publication:681335
DOI10.1016/J.CL.2015.11.001zbMATH Open1379.68239OpenAlexW2192877587MaRDI QIDQ681335FDOQ681335
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
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
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Counterexample-guided abstraction refinement for symbolic model checking
- Nested interpolants
- Constraint-based deductive model checking
- Widening with Thresholds for Programs with Complex Control Graphs
- Refinement of Trace Abstraction
- Failure tabled constraint logic programming by interpolation
- Automatically Refining Abstract Interpretations
- Logic Programming
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
- Title not available (Why is that?)
- 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
Uses Software
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)
