Symbolic Model Construction for Saturated Constrained Horn Clauses

Cites Work

Unnamed Item
Unnamed Item
Unnamed Item
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
Refutational theorem proving for hierarchic first-order theories
An efficient subsumption test pipeline for BS(LRA) clauses
Hierarchic superposition revisited
Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
Automated model building
A lattice-theoretical fixpoint theorem and its applications
Generalized Property Directed Reachability
Automated complexity analysis based on ordered resolution
Horn Clause Solvers for Program Verification
Applying Linear Quantifier Elimination
Automated Reasoning Building Blocks
Integrating Linear Arithmetic into Superposition Calculus
Superposition Modulo Linear Arithmetic SUP(LA)
Decision procedures and model building in equational clause logic
Horn clauses as an intermediate representation for program analysis and transformation
Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
Hyperresolution and automated model building
Concolic Testing in CLP
Some applications of the notions of forcing and generic sets
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
Syntax-guided termination analysis
Analysis and Transformation of Constrained Horn Clauses for Program Verification

This page was built for publication: Symbolic Model Construction for Saturated Constrained Horn Clauses