Spacer
From MaRDI portal
Cited in
(70)- Pono
- CLN2INV
- LOGEN
- FLATA
- Yices
- Solving quantified linear arithmetic by counterexample-guided instantiation
- z3
- PURRS
- Princess
- ATGen
- SMTInterpol
- Ultimate Automizer
- PeRIPLO
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Toward neural-network-guided program synthesis and verification
- Symbolic automatic relations and their applications to SMT and CHC solving
- UFO
- Eldarica
- Aligators
- HMC
- Learning inductive invariants by sampling from frequency distributions
- Refutation-based synthesis in SMT
- A layered algorithm for quantifier elimination from linear modular constraints
- Mcmt
- Ciao
- CiaoPP
- FOCI
- PrologCheck
- Horn clause solvers for program verification
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- SeaHorn
- OpenSMT2
- c2i
- Houdini
- HyComp
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- CoVaC
- MoCHi
- VeriMAP
- TyPiCal
- CTIGAR
- RAHFT
- JayHorn
- Qlose
- Rosette
- LiquidHaskell
- iSAT
- FlashMeta
- RVT
- Booster
- Rust2Viper
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- RustHorn: CHC-based verification for Rust programs
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- SMT-based model checking for recursive programs
- Bex
- Mjollnir
- nncontroller
- scientific article; zbMATH DE number 7589540 (Why is no real title available?)
- ICE-based refinement type discovery for higher-order functional programs
- Ivy
- TreeAutomizer
- eThor
- Code2Inv
- RustHorn
- On recursion-free Horn clauses and Craig interpolation
- 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
This page was built for software: Spacer
