Yices
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Don't care words with an application to the automata-based approach for real addition
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Beaver
- Boolector
- CoCoALib
- CPBPV
- GAVS
- GNT
- HOL-Boogie
- jETI
- JMLUnit
- MiniSat
- TotemBioNet
- iRankFinder
- Whiley
- Sparrow Scheduler
- MedleySolver
- SMT Kit
- BtorMC
- lazybv2int
- metaSMT
- SBV
- CoLoMoTo
- Reveal
- SDSAT
- SYNRAC
- TESTAS
- Cogent
- Prosper
- BarcelogicTools
- WoLFram
- LOGEN
- SMT-LIB
- FLATA
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Computing and estimating the volume of the solution space of SMT(LA) constraints
- Solving linear optimization over arithmetic constraint formula
- UCLID
- New techniques for linear arithmetic: cubes and equalities
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Propagation based local search for bit-precise reasoning
- Randomized algorithms for finding the shortest negative cost cycle in networks
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Cutting the mix
- cvc3
- z3
- Alt-Ergo
- KLEE
- Dagger
- Aspic
- SIMPLIFY
- LogMIP
- Parallelizing SMT solving: lazy decomposition and conciliation
- PPL
- PURRS
- libpoly
- Positive solutions of systems of signed parametric polynomial inequalities
- Probably half true: probabilistic satisfiability over Łukasiewicz infinitely-valued logic
- MiniZinc
- FlatZinc
- ASASP
- GiNaCRA
- bv2epr
- dReal
- ESC4
- GATeL
- DART
- Eclat
- ATGen
- veriT
- SMTInterpol
- Ultimate Automizer
- CVC Lite
- csp2B
- AProVE
- Sharpening constraint programming approaches for bit-vector theory
- A superposition calculus for abductive reasoning
- Fault localization of timed automata using maximum satisfiability
- OpenSMT
- On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
- On solving quantified bit-vector constraints using invertibility conditions
- SYMBA
- SAT modulo discrete event simulation applied to railway design capacity analysis
- New records of pre-image search of reduced SHA-1 using SAT solvers
- StarExec
- On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
- An SMT theory of fixed-point arithmetic
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Verifying Whiley programs with Boogie
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- \textsc{LTL} falsification in infinite-state systems
- Supercharging plant configurations using Z3
- Smt-Switch: a solver-agnostic C++ API for SMT solving
- MedleySolver: online SMT algorithm selection
- Runtime complexity analysis of logically constrained rewriting
- URBiVA
- MathSAT
- LLBMC
This page was built for software: Yices
