Cited in
(46)- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- Adapting real quantifier elimination methods for conflict set computation
- Building bridges between symbolic computation and satisfiability checking
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Algorithmic reduction of biological networks with multiple time scales
- Fully incremental cylindrical algebraic decomposition
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- CoCoALib
- QEPCAD
- SYNRAC
- SMT-LIB
- REDLOG
- Yices
- Orbital library
- libpoly
- GiNaCRA
- dReal
- veriT
- NLTOOLBOX
- MathSAT5
- PARAM
- CArL
- CalCS
- raSAT
- EFSMT
- Theoryguru
- XSat
- HyPro
- iSAT
- CylindricalAlgebraicDecompose
- PRISM-PSY
- FACT
- Positive solutions of systems of signed parametric polynomial inequalities
- On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
- jsCoq
- raSAT: An SMT Solver for Polynomial Constraints
- Polynomial constraints and unsat cores in \textsc{Tarski}
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Zephyrus2
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
This page was built for software: SMT-RAT
