Satisfiability modulo theories
From MaRDI portal
Recommendations
Cites work
- A comprehensive combination framework
- A Compressing Translation from Propositional Resolution to Natural Deduction
- A Computing Procedure for Quantification Theory
- A Decision Procedure for Bit-Vectors and Arrays
- A machine program for theorem-proving
- A mathematical introduction to logic.
- A Reachability Predicate for Analyzing Low-Level Software
- An abstract decision procedure for a theory of inductive data types.
- An abstract interpretation of DPLL(T)
- An instantiation scheme for satisfiability modulo theories
- An interpolating theorem prover
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- BDD-based symbolic model checking
- Boolean satisfiability with transitivity constraints
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Bounded model checking using satisfiability solving
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Combined Satisfiability Modulo Parametric Theories
- Combining decision procedures.
- Combining nonstably infinite theories
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Complexity, convexity and combinations of theories
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computing small unsatisfiable cores in satisfiability modulo theories
- Conflict Resolution
- Constraint solving for interpolation
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Deciding Bit-Vector Arithmetic with Abstraction
- Decision Procedures for Multisets with Cardinality Constraints
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- dReal: an SMT solver for nonlinear theories over the reals
- Efficiency of a Good But Not Linear Set Union Algorithm
- Efficient E-Matching for SMT Solvers
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Efficient theory combination via Boolean search
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- Fast congruence closure and extensions
- Fast Decision Procedures Based on Congruence Closure
- Fast LCF-Style Proof Reconstruction for Z3
- Frontiers of Combining Systems
- Generalizing DPLL to Richer Logics
- Ground Interpolation for Combined Theories
- Ground Interpolation for the Theory of Equality
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- scientific article; zbMATH DE number 1140674 (Why is no real title available?)
- scientific article; zbMATH DE number 1956605 (Why is no real title available?)
- scientific article; zbMATH DE number 1979548 (Why is no real title available?)
- scientific article; zbMATH DE number 1979549 (Why is no real title available?)
- scientific article; zbMATH DE number 1507186 (Why is no real title available?)
- scientific article; zbMATH DE number 1931669 (Why is no real title available?)
- scientific article; zbMATH DE number 1903346 (Why is no real title available?)
- scientific article; zbMATH DE number 1903355 (Why is no real title available?)
- scientific article; zbMATH DE number 1903356 (Why is no real title available?)
- scientific article; zbMATH DE number 2090300 (Why is no real title available?)
- scientific article; zbMATH DE number 2102726 (Why is no real title available?)
- scientific article; zbMATH DE number 2102727 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Interpolation and model checking
- Interpolation and SAT-based model checking.
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Lazy satisfiability modulo theories
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logics in Artificial Intelligence
- Lower bounds for resolution and cutting plane proofs and monotone computations
- MCMT: a model checker modulo theories
- Mechanizing Mathematical Reasoning
- Model Checking Software
- Model-based theory combination
- Model-theoretic methods in combined constraint satisfiability
- More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
- Negative-cycle detection algorithms
- On SAT Modulo Theories and Optimization Problems
- Polite theories revisited
- Predicate abstraction for program verification
- Proof tree preserving interpolation
- Quantifier instantiation techniques for finite model finding in SMT
- Resolution proof transformation for compression and interpolation
- Rocket-Fast Proof Checking for SMT Solvers
- SAT-Based Model Checking
- Simplification by Cooperating Decision Procedures
- Simplify: a theorem prover for program checking
- SMT proof checking using a logical framework
- Solvable cases of the decision problem
- Solving non-linear arithmetic
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Splitting on Demand in SAT Modulo Theories
- Term Rewriting and All That
- The MathSAT5 SMT solver
- Theorem proving using lazy proof explication.
- Theory and Applications of Satisfiability Testing
- Theory Instantiation
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Towards SMT Model Checking of Array-Based Systems
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Variations on the Common Subexpression Problem
- Verification, Model Checking, and Abstract Interpretation
Cited in
(only showing first 100 items - show all)- A framework for satisfiability modulo theories
- Solving quantified verification conditions using satisfiability modulo theories
- Model learning as a satisfiability modulo theories problem
- Designing theory solvers with extensions
- Deciding local theory extensions via E-matching
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- The complexity of verifying population protocols
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Politeness and stable infiniteness: stronger together
- Multi-dimensional interpretations for termination of term rewriting
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Tuple interpretations for termination of term rewriting
- Flexible proof production in an industrial-strength SMT solver
- Reasoning about vectors using an SMT theory of sequences
- Towards finding longer proofs
- Automatic synthesis of data-flow analyzers
- Correct approximation of IEEE 754 floating-point arithmetic for program verification
- A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- An SMT-based approach for verifying binarized neural networks
- Unbounded procedure summaries from bounded environments
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- Satisfiability modulo transcendental functions via incremental linearization
- Satisfiability modulo bounded checking
- Modular strategic SMT solving with \textbf{SMT-RAT}
- A bit-vector differential model for the modular addition by a constant
- A practical approach to satisfiability modulo linear integer arithmetic
- A survey of satisfiability modulo theory
- \textsf{TSAT++}: an open platform for satisfiability modulo theories
- Using satisfiability modulo theories for inductive verification of Lustre programs
- An experiment with satisfiability modulo SAT
- Taking satisfiability to the next level with Z3 (abstract)
- Virtual substitution for SMT-solving
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Temporal logic and fair discrete systems
- Binary decision diagrams
- SAT-Based Model Checking
- Combining Model Checking and Deduction
- scientific article; zbMATH DE number 6528599 (Why is no real title available?)
- Lazy satisfiability modulo theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Satisfiability modulo the theory of costs: foundations and applications
- Beyond satisfiability: extensions and applications
- Instantiation of SMT problems modulo integers
- Natural domain SMT: a preliminary assessment
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- ${\mathcal{T}}$ -Decision by Decomposition
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Satisfiability modulo theories: an appetizer
- An instantiation scheme for satisfiability modulo theories
- Satisfiability checking: theory and applications
- Separation logics and modalities: a survey
- Precise and complete propagation based local search for satisfiability modulo theories
- Solving constraint satisfaction problems with SAT modulo theories
- A system for solving constraint satisfaction problems with SMT
- Foundations of satisfiability modulo theories
- A logic-based framework leveraging neural networks for studying the evolution of neurological disorders
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- MILP, pseudo-Boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks
- Decision procedures. An algorithmic point of view
- The problem of checking the satisfiability of formulae of decidable theories (survey)
- Modal Satisfiability via SMT Solving
- SMC: satisfiability modulo convex optimization
- The MathSAT5 SMT solver
- A modular approach to MaxSAT modulo theories
- Splitting on Demand in SAT Modulo Theories
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- A Tutorial on Satisfiability Modulo Theories
- Challenges in Satisfiability Modulo Theories
- An Abstract Framework for Satisfiability Modulo Theories
- Rocket-Fast Proof Checking for SMT Solvers
- Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
- Computer Aided Verification
- Computer Aided Verification
- MCMT: a model checker modulo theories
- Bugs, moles and skeletons: symbolic reasoning for software development
- On SAT Modulo Theories and Optimization Problems
- From Propositional Satisfiability to Satisfiability Modulo Theories
- A Progressive Simplifier for Satisfiability Modulo Theories
- Combined Satisfiability Modulo Parametric Theories
- A Practical Approach to Discretised PDDL+ Problems by Translation to Numeric Planning
- Reasoning about vectors: satisfiability modulo a theory of sequences
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Risk-aware shielding of partially observable Monte Carlo planning policies
- A solver for arrays with concatenation
- SMT sampling via model-guided approximation
- Verified verifying: SMT-LIB for strings in Isabelle
- SAT Modulo Differential Equation Simulations
- Even Faster Conflicts and Lazier Reductions for String Solvers
- Local Search for SMT on Linear Integer Arithmetic
- Adversarial reachability for program-level security analysis
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Cryptanalysis of \texttt{SPEEDY}
- Bitwuzla
- Fast approximations of quantifier elimination
- Satisfiability modulo finite fields
Describes a project that uses
Uses Software
This page was built for publication: Satisfiability modulo theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176369)
