The following pages link to Solving Non-linear Arithmetic (Q2908506):
Displayed 50 items.
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Barrier certificates revisited (Q507352) (← links)
- Structured learning modulo theories (Q511777) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Learning probabilistic termination proofs (Q832245) (← links)
- Interpolation and model checking for nonlinear arithmetic (Q832268) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- raSAT: an SMT solver for polynomial constraints (Q1688535) (← links)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (Q1996869) (← links)
- Using machine learning to improve cylindrical algebraic decomposition (Q2009221) (← links)
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q2055849) (← links)
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Counterexample- and simulation-guided floating-point loop invariant synthesis (Q2233532) (← links)
- Learning modulo theories for constructive preference elicitation (Q2238637) (← links)
- A conflict-driven solving procedure for poly-power constraints (Q2303230) (← links)
- Conflict-driven satisfiability for theory combination: transition system and completeness (Q2303254) (← links)
- Editorial: Symbolic computation and satisfiability checking (Q2307620) (← links)
- Fully incremental cylindrical algebraic decomposition (Q2307621) (← links)
- Cylindrical algebraic decomposition with equational constraints (Q2307622) (← links)
- From simplification to a partial theory solver for non-linear real polynomial constraints (Q2307623) (← links)
- Applying computer algebra systems with SAT solvers to the Williamson conjecture (Q2307627) (← links)
- Constructing a single cell in cylindrical algebraic decomposition (Q2343239) (← links)
- Modular strategic SMT solving with \textbf{SMT-RAT} (Q2414693) (← links)
- Automated analysis of cryptographic assumptions in generic group models (Q2423840) (← links)
- Deniable Functional Encryption (Q2798776) (← links)
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation (Q2817292) (← links)
- raSAT: An SMT Solver for Polynomial Constraints (Q2817923) (← links)
- Speeding up the Constraint-Based Method in Difference Logic (Q2818021) (← links)
- Quantitative Abstractions for Collective Adaptive Systems (Q2822665) (← links)
- Efficient Simplification Techniques for Special Real Quantifier Elimination with Applications to the Synthesis of Optimal Numerical Algorithms (Q2830000) (← links)
- A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
- Solving Nonlinear Integer Arithmetic with MCSAT (Q2961575) (← links)
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation (Q2964460) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Are Parametric Markov Chains Monotonic? (Q3297607) (← links)
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF (Q3303890) (← links)
- Sequential Convex Programming for the Efficient Verification of Parametric MDPs (Q3303926) (← links)
- Recent Advances in Real Geometric Reasoning (Q3452275) (← links)
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (Q3453240) (← links)
- Satisfiability Checking: Theory and Applications (Q4571125) (← links)
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness (Q5014692) (← links)
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition (Q5495916) (← links)
- Symbolic computation of differential equivalences (Q5920213) (← links)
- Truth table invariant cylindrical algebraic decomposition (Q5963392) (← links)
- Cylindrical algebraic decomposition using local projections (Q5963393) (← links)
- Verification Modulo theories (Q6056642) (← links)
- Automated analysis of tethered DNA nanostructures using constraint solving (Q6062022) (← links)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893) (← links)
- From Polynomial Invariants to Linear Loops (Q6081960) (← links)