\texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
DOI10.1007/978-3-319-24318-4_26zbMATH Open1471.68241OpenAlexW2277676404MaRDI QIDQ3453240FDOQ3453240
Authors: Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám 
Publication date: 20 November 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_26
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Theory and Applications of Satisfiability Testing
- CoCoALib: A C++ library for computations in commutative algebra\(\dots \) and beyond
- Introduction to the GiNaC framework for symbolic computation within the \(\text{C}^{++}\) programming language
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- The MathSAT5 SMT solver
- Lazy satisfiability modulo theories
- Algorithms in real algebraic geometry
- Satisfiability of non-linear (ir)rational arithmetic
- Solving non-linear arithmetic
- Real World Verification
- MetiTarski: An automatic theorem prover for real-valued special functions
- The complexity of linear problems in fields
- Simplification of quantifier-free formulae over ordered fields
- Title not available (Why is that?)
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Title not available (Why is that?)
- On the Theoretical and Practical Complexity of the Existential Theory of Reals
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- Virtual substitution for SMT-solving
- Proving termination of programs automatically with AProVE
- The strategy challenge in SMT solving
- On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
Cited In (24)
- 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
- Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
- The strategy challenge in SMT solving
- 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
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Algorithmic reduction of biological networks with multiple time scales
- \textsf{PFL}: a probabilistic logic for fault trees
- Fully incremental cylindrical algebraic decomposition
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- SMT-RAT
- Satisfiability checking: theory and applications
- 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
- Satisfiability modulo finite fields
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
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)
