A Survey of Satisfiability Modulo Theory (Q2830018): Difference between revisions

@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Algorithms in real algebraic geometry
@@ Property / cites work: Algorithms in real algebraic geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Linear Quantifier Elimination as an Abstract Decision Procedure
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding floating-point logic with abstract conflict driven clause learning
+Normal rank
@@ Property / cites work @@
+A BLAS based C library for exact linear algebra on integer matrices
+Normal rank
@@ Property / cites work @@
+Proof Tree Preserving Interpolation
@@ Property / cites work: Proof Tree Preserving Interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5674430
@@ Property / cites work: Q5674430 / rank @@
+Normal rank
@@ Property / cites work @@
+Natural Domain SMT: A Preliminary Assessment
@@ Property / cites work: Natural Domain SMT: A Preliminary Assessment / rank @@
+Normal rank
@@ Property / cites work @@
+Generating Non-linear Interpolants by Semidefinite Programming
+Normal rank
@@ Property / cites work @@
+Linear Programming
@@ Property / cites work: Linear Programming / rank @@
+Normal rank
@@ Property / cites work @@
+A Model-Constructing Satisfiability Calculus
@@ Property / cites work: A Model-Constructing Satisfiability Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
+Normal rank
@@ Property / cites work @@
+SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for the First Order Theory of Real Addition with Order
+Normal rank
@@ Property / cites work @@
+Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
+Normal rank
@@ Property / cites work @@
+Solving systems of polynomial inequalities in subexponential time
+Normal rank
@@ Property / cites work @@
+The intractability of resolution
@@ Property / cites work: The intractability of resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Representing polynomials by positive linear functions on compact convex polyhedra
+Normal rank
@@ Property / cites work @@
+Playing in the grey area of proofs
@@ Property / cites work: Playing in the grey area of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic execution and program testing
@@ Property / cites work: Symbolic execution and program testing / rank @@
+Normal rank
@@ Property / cites work @@
+Anneaux preordonnes
@@ Property / cites work: Anneaux preordonnes / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
+Normal rank
@@ Property / cites work @@
+Applying Linear Quantifier Elimination
@@ Property / cites work: Applying Linear Quantifier Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
+Normal rank
@@ Property / cites work @@
+Q4391223
@@ Property / cites work: Q4391223 / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Generalizing DPLL to Richer Logics
@@ Property / cites work: Generalizing DPLL to Richer Logics / rank @@
+Normal rank
@@ Property / cites work @@
+A Quantifier Elimination Algorithm for Linear Real Arithmetic
+Normal rank
@@ Property / cites work @@
+On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
+Normal rank
@@ Property / cites work @@
+Q4660671
@@ Property / cites work: Q4660671 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4221106
@@ Property / cites work: Q4221106 / rank @@
+Normal rank
@@ Property / cites work @@
+Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
+Normal rank
@@ Property / cites work @@
+Q3412521
@@ Property / cites work: Q3412521 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3141916
@@ Property / cites work: Q3141916 / rank @@
+Normal rank