SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
From MaRDI portal
Publication:3453240
DOI10.1007/978-3-319-24318-4_26zbMath1471.68241OpenAlexW2277676404MaRDI QIDQ3453240
Gereon Kremer, Florian Corzilius, Erika Ábrahám, Sebastian Junges, Stefan Schupp
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
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Satisfiability Checking: Theory and Applications ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Experiments with automated reasoning in the class ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ \textsf{PFL}: a probabilistic logic for fault trees ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Fully incremental cylindrical algebraic decomposition ⋮ SMT-RAT ⋮ Efficient Simplification Techniques for Special Real Quantifier Elimination with Applications to the Synthesis of Optimal Numerical Algorithms ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- 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
- Introduction to the GiNaC framework for symbolic computation within the \(\text{C}^{++}\) programming language
- On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
- Solving Non-linear Arithmetic
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Virtual Substitution for SMT-Solving
- On the Theoretical and Practical Complexity of the Existential Theory of Reals
- Proving Termination of Programs Automatically with AProVE
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- The Strategy Challenge in SMT Solving
- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
- Real World Verification
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT Solver
- CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
- Algorithms in real algebraic geometry
