swMATH4436MaRDI QIDQ16612FDOQ16612
Author name not available (Why is that?)
Official website: http://yices.csl.sri.com/
Cited In (only showing first 100 items - show all)
- Extending Sledgehammer with SMT solvers
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Automatic generation of logical models with AGES
- Boolector
- GAVS
- GNT
- HOL-Boogie
- SDSAT
- TESTAS
- Cogent
- Prosper
- WoLFram
- SMT-LIB
- Alt-Ergo
- cvc3
- Aspic
- KLEE
- Dagger
- UCLID
- LogMIP
- SIMPLIFY
- z3
- PPL
- PURRS
- libpoly
- FlatZinc
- MiniZinc
- ASASP
- GiNaCRA
- bv2epr
- dReal
- ESC4
- ATGen
- DART
- GATeL
- Eclat
- SMTInterpol
- veriT
- Ultimate Automizer
- TRACER
- CVC Lite
- csp2B
- AProVE
- OpenSMT
- SYMBA
- StarExec
- CVC4
- MathSAT
- LLBMC
- ABC
- MathSAT5
- Aligators
- Eldarica
- MFE
- isl
- GIST
- CiME
- HSF
- Anima
- URBiVA
- PolyLib
- Proteus
- MINION
- Saigawa
- Sugar
- Monotonox
- TLPVS
- CSIsat
- tawSolver
- Ltur
- HybridSal
- Mcmt
- SIMPLY
- NSPLib
- Skeptik
- Jahob
- CCASat
- FOCI
- CArL
- CalCS
- PRALINE
- PRISM-games
- SMT-RAT
- SAL
- fzn2smt
- JViews
- Cubicle
- FreeRTOS
- Ctrl
- PrologCheck
- raSAT
- KITTeL
- FME-IT
- SeaHorn
- nuXmv
- Solving constraint satisfaction problems with SAT modulo theories
- Probably half true: probabilistic satisfiability over Łukasiewicz infinitely-valued logic
- Automatic proof and disproof in Isabelle/HOL
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
This page was built for software: Yices
