Solving constrained Horn clauses using dependence-disjoint expansions

MaRDI QIDQ3384902FDOQ3384902

Authors:

Publication date: 17 December 2021

Full work available at URL: https://arxiv.org/abs/1705.03167

Recommendations

• Synchronizing constrained Horn clauses
• Solving constrained Horn clauses over algebraic data types
• Solving Horn clauses on inductive data types without induction

Mathematics Subject Classification ID

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

Cites Work

• Nested interpolants
• An interpolating theorem prover
• Lazy Abstraction with Interpolants
• On recursion-free Horn clauses and Craig interpolation
• Generalized property directed reachability
• Avoiding exponential explosion: generating compact verification conditions
• Whale: an interpolation-based algorithm for inter-procedural verification
• SMT-based model checking for recursive programs
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Reachability modulo theories

Cited In (7)

• Title not available (Why is that?)
• Autark assignments of Horn CNFs
• Solving constrained Horn clauses over algebraic data types
• On a generalization of Horn constraint systems
• Title not available (Why is that?)
• An algorithm to compute maximal contractions for Horn clauses
• Maximizing branch coverage with constrained Horn clauses

This page was built for publication: Solving constrained Horn clauses using dependence-disjoint expansions

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