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