CVC4
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Apron
- Beaver
- Boolector
- CoCoALib
- CPBPV
- CUTE
- Dafny
- D-Finder
- LEO-II
- MiniSat
- PAYNT
- Nitpick
- PReLearn
- lazyCoP
- StringFuzz
- ZaligVinder
- AMulet
- Goeland
- FRAT
- Shellcheck
- CoLiS
- MedleySolver
- SMT Kit
- BtorMC
- lazybv2int
- metaSMT
- Pono
- SBV
- Smt-Switch
- QBFFam
- LP3Verif
- Q3B
- Paracooba
- Kissat
- CLN2INV
- Nunchaku
- SDSAT
- SYNRAC
- LOGEN
- VAMPIRE
- Paradox
- A set solver for finite set relation algebra
- SMT-LIB
- SPASS
- A formally verified interpreter for a shell-like programming language
- TPTP
- REDLOG
- Instrumenting a weakest precondition calculus for counterexample generation
- Punf
- Computing and estimating the volume of the solution space of SMT(LA) constraints
- Yices
- Why3
- Metis
- A deontic logic reasoning infrastructure
- Solving linear optimization over arithmetic constraint formula
- Frama-C
- Automatically improving constraint models in Savile Row
- SATIRE
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- New techniques for linear arithmetic: cubes and equalities
- Propagation based local search for bit-precise reasoning
- Reasoning about algebraic data types with abstractions
- Cutting the mix
- Counterexample-guided quantifier instantiation for synthesis in SMT
- z3
- Alt-Ergo
- LLVM
- KLEE
- SIMPLIFY
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- Parallelizing SMT solving: lazy decomposition and conciliation
- Orbital library
- libpoly
- Positive solutions of systems of signed parametric polynomial inequalities
- Unifying separation logic and region logic to allow interoperability
- The satisfiability of word equations: decidable and undecidable theories
- A generic framework for implicate generation modulo theories
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- A reduction from unbounded linear mixed arithmetic problems into bounded problems
- Superposition with datatypes and codatatypes
- Datatypes with shared selectors
- OCaml
- PoCaB
- Cadmium
- GiNaCRA
- Zenon
- Satallax
- Princess
- Sledgehammer
- ProB
- Kodkod
- Scala
- PathCrawler
- DART
- ATGen
- veriT
- TaPAS
- SMTInterpol
This page was built for software: CVC4
