Satisfiability Modulo Theories (Q3176369): Difference between revisions

@@ Property / describes a project that uses @@
+Yices
@@ Property / describes a project that uses: Yices / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CLSAT
@@ Property / describes a project that uses: CLSAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MathSAT5
@@ Property / describes a project that uses: MathSAT5 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+iProver
@@ Property / describes a project that uses: iProver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FOCI
@@ Property / describes a project that uses: FOCI / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Beaver
@@ Property / describes a project that uses: Beaver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cvc3
@@ Property / describes a project that uses: cvc3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+veriT
@@ Property / describes a project that uses: veriT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMTInterpol
@@ Property / describes a project that uses: SMTInterpol / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Boolector
@@ Property / describes a project that uses: Boolector / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+dReal
@@ Property / describes a project that uses: dReal / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenSMT
@@ Property / describes a project that uses: OpenSMT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HAMPI
@@ Property / describes a project that uses: HAMPI / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mcmt
@@ Property / describes a project that uses: Mcmt / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+STP
@@ Property / describes a project that uses: STP / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-319-10575-8_11
+Normal rank
@@ Property / OpenAlex ID @@
+W1481397690
@@ Property / OpenAlex ID: W1481397690 / rank @@
+Normal rank
@@ Property / cites work @@
+Solvable cases of the decision problem
@@ Property / cites work: Solvable cases of the decision problem / rank @@
+Normal rank
@@ Property / cites work @@
+A Compressing Translation from Propositional Resolution to Natural Deduction
+Normal rank
@@ Property / cites work @@
+Mechanizing Mathematical Reasoning
@@ Property / cites work: Mechanizing Mathematical Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Model Checking Software
@@ Property / cites work: Model Checking Software / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809056
@@ Property / cites work: Q4809056 / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Splitting on Demand in SAT Modulo Theories
@@ Property / cites work: Splitting on Demand in SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q5309032
@@ Property / cites work: Q5309032 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804899
@@ Property / cites work: Q4804899 / rank @@
+Normal rank
@@ Property / cites work @@
+Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
+Normal rank
@@ Property / cites work @@
+Q4417953
@@ Property / cites work: Q4417953 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking
@@ Property / cites work: SAT-Based Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+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 @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient theory combination via Boolean search
@@ Property / cites work: Efficient theory combination via Boolean search / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+An Abstract Interpretation of DPLL(T)
@@ Property / cites work: An Abstract Interpretation of DPLL(T) / rank @@
+Normal rank
@@ Property / cites work @@
+Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
+Normal rank
@@ Property / cites work @@
+Resolution proof transformation for compression and interpolation
+Normal rank
@@ Property / cites work @@
+Q4804887
@@ Property / cites work: Q4804887 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4818814
@@ Property / cites work: Q4818814 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding Bit-Vector Arithmetic with Abstraction
@@ Property / cites work: Deciding Bit-Vector Arithmetic with Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Boolean satisfiability with transitivity constraints
+Normal rank
@@ Property / cites work @@
+Q4503906
@@ Property / cites work: Q4503906 / rank @@
+Normal rank
@@ Property / cites work @@
+BDD-Based Symbolic Model Checking
@@ Property / cites work: BDD-Based Symbolic Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+A Reachability Predicate for Analyzing Low-Level Software
+Normal rank
@@ Property / cites work @@
+Negative-cycle detection algorithms
@@ Property / cites work: Negative-cycle detection algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Tree Preserving Interpolation
@@ Property / cites work: Proof Tree Preserving Interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Interpolant Generation in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Efficient generation of craig interpolants in satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Bounded model checking using satisfiability solving
+Normal rank
@@ Property / cites work @@
+Fast and Flexible Difference Constraint Propagation for DPLL(T)
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / 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 @@
+Variations on the Common Subexpression Problem
@@ Property / cites work: Variations on the Common Subexpression Problem / rank @@
+Normal rank
@@ Property / cites work @@
+An instantiation scheme for satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+Q2703808
@@ Property / cites work: Q2703808 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
+Normal rank
@@ Property / cites work @@
+Ground Interpolation for the Theory of Equality
@@ Property / cites work: Ground Interpolation for the Theory of Equality / rank @@
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Bit-Vectors and Arrays
@@ Property / cites work: A Decision Procedure for Bit-Vectors and Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Theory Instantiation
@@ Property / cites work: Theory Instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+dReal: An SMT Solver for Nonlinear Theories over the Reals
+Normal rank
@@ Property / cites work @@
+Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Model-theoretic methods in combined constraint satisfiability
+Normal rank
@@ Property / cites work @@
+Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
+Normal rank
@@ Property / cites work @@
+Towards SMT Model Checking of Array-Based Systems
@@ Property / cites work: Towards SMT Model Checking of Array-Based Systems / rank @@
+Normal rank
@@ Property / cites work @@
+A comprehensive combination framework
@@ Property / cites work: A comprehensive combination framework / rank @@
+Normal rank
@@ Property / cites work @@
+MCMT: A Model Checker Modulo Theories
@@ Property / cites work: MCMT: A Model Checker Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Ground Interpolation for Combined Theories
@@ Property / cites work: Ground Interpolation for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Predicate Abstraction for Program Verification
@@ Property / cites work: Predicate Abstraction for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Polite Theories Revisited
@@ Property / cites work: Polite Theories Revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+Conflict Resolution
@@ Property / cites work: Conflict Resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
+Normal rank
@@ Property / cites work @@
+Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
+Normal rank
@@ Property / cites work @@
+Combined Satisfiability Modulo Parametric Theories
+Normal rank
@@ Property / cites work @@
+Q4427901
@@ Property / cites work: Q4427901 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods at the Crossroads. From Panacea to Foundational Support
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation and Model Checking
@@ Property / cites work: Interpolation and Model Checking / 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 @@
+Rocket-Fast Proof Checking for SMT Solvers
@@ Property / cites work: Rocket-Fast Proof Checking for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Model-based Theory Combination
@@ Property / cites work: Model-based Theory Combination / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+On SAT Modulo Theories and Optimization Problems
@@ Property / cites work: On SAT Modulo Theories and Optimization Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Fast congruence closure and extensions
@@ Property / cites work: Fast congruence closure and extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Complexity, convexity and combinations of theories
+Normal rank
@@ Property / cites work @@
+Decision Procedures for Multisets with Cardinality Constraints
+Normal rank
@@ Property / cites work @@
+Q4818813
@@ Property / cites work: Q4818813 / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+Frontiers of Combining Systems
@@ Property / cites work: Frontiers of Combining Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifier Instantiation Techniques for Finite Model Finding in SMT
+Normal rank
@@ Property / cites work @@
+Constraint solving for interpolation
@@ Property / cites work: Constraint solving for interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3818127
@@ Property / cites work: Q3818127 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3506045
@@ Property / cites work: Q3506045 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4427902
@@ Property / cites work: Q4427902 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804898
@@ Property / cites work: Q4804898 / rank @@
+Normal rank
@@ Property / cites work @@
+SMT proof checking using a logical framework
@@ Property / cites work: SMT proof checking using a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiency of a Good But Not Linear Set Union Algorithm
+Normal rank
@@ Property / cites work @@
+Q4708927
@@ Property / cites work: Q4708927 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385439
@@ Property / cites work: Q4385439 / rank @@
+Normal rank
@@ Property / cites work @@
+Unions of non-disjoint theories and combinations of satisfiability procedures
+Normal rank
@@ Property / cites work @@
+Logics in Artificial Intelligence
@@ Property / cites work: Logics in Artificial Intelligence / rank @@
+Normal rank
@@ Property / cites work @@
+Combining nonstably infinite theories
@@ Property / cites work: Combining nonstably infinite theories / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3176369