Spacer
From MaRDI portal
Software:31323
No author found.
Related Items (21)
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ RustHorn: CHC-Based Verification for Rust Programs ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Programmable program synthesis ⋮ Constraint-based relational verification ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Toward neural-network-guided program synthesis and verification ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Horn Clause Solvers for Program Verification ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Unnamed Item ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ SMT-based model checking for recursive programs ⋮ Refutation-based synthesis in SMT ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates
This page was built for software: Spacer
