Horn clause solvers for program verification
From MaRDI portal
Recommendations
Cites work
- A constraint-based approach to solving games on infinite graphs
- A Transformation System for Developing Recursive Programs
- A type-directed abstraction refinement approach to higher-order model checking
- Accelerating interpolants
- An axiomatic basis for computer programming
- An overview of Ciao and its design philosophy
- Booster: an acceleration-based verification framework for array programs
- Complexity, convexity and combinations of theories
- Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
- Efficient weakest preconditions
- Generalized property directed reachability
- scientific article; zbMATH DE number 4055578 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 1142320 (Why is no real title available?)
- scientific article; zbMATH DE number 1158761 (Why is no real title available?)
- scientific article; zbMATH DE number 236855 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- Inadequacy of computable loop invariants
- Low-level liquid types
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Model Checking Recursive Programs with Exact Predicate Abstraction
- On sentences which are true of direct unions of algebras
- Precise interprocedural dataflow analysis with applications to constant propagation
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Property directed polyhedral abstraction
- Property-directed inference of universal invariants or proving their absence
- Reasoning about procedures as parameters in the language L4
- Resourceful reachability as HORN-LA
- SAT-Based Model Checking without Unrolling
- Separation logic modulo theories
- Some characterization theorems for infinitary universal Horn logic without equality
- Soundness and Completeness of an Axiom System for Program Verification
- Superposition as a decision procedure for timed automata
- Synthesis and transformation of logic programs using unfold/fold proofs
- Temporal verification of reactive systems: response
- The concept of a supercompiler
- The Semantics of Predicate Logic as a Programming Language
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
Cited in
(83)- Sensitivity analysis for Horn formulae
- A tree-based approach to data flow proofs
- Automatic synthesis of logical models for order-sorted first-order theories
- Autark assignments of Horn CNFs
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Subsumption demodulation in first-order theorem proving
- Reasoning in the theory of heap: satisfiability and interpolation
- Toward neural-network-guided program synthesis and verification
- Symbolic automatic relations and their applications to SMT and CHC solving
- Exact and parameterized algorithms for read-once refutations in Horn constraint systems
- Loop verification with invariants and contracts
- Automating induction for solving Horn clauses
- Leveraging Horn clause solving for compositional verification of PLC software
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Analyzing read-once cutting plane proofs in Horn systems
- Proof relevant corecursive resolution
- Efficient reasoning for inconsistent Horn formulae
- Resourceful reachability as HORN-LA
- Normalization of linear Horn clauses
- Smallest horn clause programs
- Solving Horn clauses on inductive data types without induction
- Horn clauses as an intermediate representation for program analysis and transformation
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Introduction to the special issue on computational logic for verification
- Predicate pairing for program verification
- Tree dimension in verification of constrained Horn clauses
- Incremental and modular context-sensitive analysis
- Generalised interpolation by solving recursion-free Horn clauses
- Efficient CTL verification via Horn constraints solving
- scientific article; zbMATH DE number 7440191 (Why is no real title available?)
- Solving non-linear Horn clauses using a linear Horn clause solver
- Removing unnecessary variables from Horn clause verification conditions
- scientific article; zbMATH DE number 7444023 (Why is no real title available?)
- scientific article; zbMATH DE number 7453190 (Why is no real title available?)
- scientific article; zbMATH DE number 7453193 (Why is no real title available?)
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Computing abstract distances in logic programs
- scientific article; zbMATH DE number 7214004 (Why is no real title available?)
- Fold/unfold transformations for fixpoint logic
- Inferring simple solutions to recursion-free Horn clauses via sampling
- Probabilistic Horn clause verification
- Iterative Specialisation of Horn Clauses
- ICE-based refinement type discovery for higher-order functional programs
- Abstraction refinement and antichains for trace inclusion of infinite state systems
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Parameterized recursive refinement types for automated program verification
- Towards a dereversibilizer: fewer asserts, statically
- Efficient modular SMT-based model checking of pointer programs
- HoIce: an ICE-based non-linear Horn clause solver
- OptiRica: towards an efficient optimizing Horn solver
- scientific article; zbMATH DE number 7806143 (Why is no real title available?)
- Reasoning About Data Trees Using CHCs
- Termination Analysis for the \pi -Calculus by Reduction to Sequential Program Termination
- Case-free programs: An abstraction of definite horn programs
- Farkas Bounds on Horn Constraint Systems
- On Incremental Pre-processing for SMT
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Neural network-guided synthesis of recursive list functions
- The \textsc{Golem} Horn solver
- Automatic program instrumentation for automatic verification
- Temporal verification of programs via first-order fixpoint logic
- An overview of the HFL model checking project
- Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
- A fixed-point theorem for Horn formula equations
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- Computing witnesses using the SCAN algorithm
- Towards neural-network-guided program synthesis and verification
- CHC-COMP 2023: competition report
- Unfolding state variables improves model checking performance
- Catamorphic abstractions for constrained Horn clause satisfiability
- Automatic bit- and memory-precise verification of eBPF code
- Collaborative inference of combined invariants
- An abstract fixed-point theorem for Horn formula equations
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Symbol elimination and applications to parametric entailment problems
- On the copy complexity of width 3 Horn constraint systems
- Constraint-based relational verification
- Decision tree learning in CEGIS-based termination analysis
- Progress in certifying hardware model checking results
Describes a project that uses
Uses Software
This page was built for publication: Horn clause solvers for program verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2947164)
