\texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
From MaRDI portal
Publication:3453240
Recommendations
Cites work
- scientific article; zbMATH DE number 1157666 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- Algorithms in real algebraic geometry
- CoCoALib: A C++ library for computations in commutative algebra and beyond
- Introduction to the GiNaC framework for symbolic computation within the \(\text{C}^{++}\) programming language
- Lazy satisfiability modulo theories
- MetiTarski: An automatic theorem prover for real-valued special functions
- On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
- On the Theoretical and Practical Complexity of the Existential Theory of Reals
- Proving termination of programs automatically with AProVE
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Real World Verification
- Satisfiability of non-linear (ir)rational arithmetic
- Simplification of quantifier-free formulae over ordered fields
- Solving non-linear arithmetic
- The MathSAT5 SMT solver
- The complexity of linear problems in fields
- The strategy challenge in SMT solving
- Theory and Applications of Satisfiability Testing
- Virtual substitution for SMT-solving
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
Cited in
(28)- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- Parameter synthesis for Markov models: covering the parameter space
- Levelwise construction of a single cylindrical algebraic cell
- FMplex: exploring a bridge between Fourier-Motzkin and simplex
- Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- The strategy challenge in SMT solving
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Algorithmic reduction of biological networks with multiple time scales
- Divide and conquer: variable set separation in hybrid systems reachability analysis
- Fully incremental cylindrical algebraic decomposition
- \textsf{PFL}: a probabilistic logic for fault trees
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- SMT-RAT
- Satisfiability checking: theory and applications
- More is less: adding polynomials for faster explanations in NLSAT
- SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
- Verified Quadratic Virtual Substitution for Real Arithmetic
- Experiments with automated reasoning in the class
- Extending the fundamental theorem of linear programming for strict inequalities
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Satisfiability modulo finite fields
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Modular strategic SMT solving with \textbf{SMT-RAT}
- FMplex: a novel method for solving linear real arithmetic problems
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
Describes a project that uses
Uses Software
This page was built for publication: \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453240)
