Satisfiability modulo theories
From MaRDI portal
Recommendations
Cites work
- 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?)
- A Compressing Translation from Propositional Resolution to Natural Deduction
- A Computing Procedure for Quantification Theory
- A Decision Procedure for Bit-Vectors and Arrays
- A Reachability Predicate for Analyzing Low-Level Software
- A comprehensive combination framework
- A machine program for theorem-proving
- A mathematical introduction to logic.
- 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)
- Efficiency of a Good But Not Linear Set Union Algorithm
- Efficient E-Matching for SMT Solvers
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Efficient theory combination via Boolean search
- Fast Decision Procedures Based on Congruence Closure
- Fast LCF-Style Proof Reconstruction for Z3
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- Fast congruence closure and extensions
- Frontiers of Combining Systems
- Generalizing DPLL to Richer Logics
- Ground Interpolation for Combined Theories
- Ground Interpolation for the Theory of Equality
- Interpolation and SAT-based model checking.
- Interpolation and model checking
- 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
- SMT proof checking using a logical framework
- Simplification by Cooperating Decision Procedures
- Simplify: a theorem prover for program checking
- Solvable cases of the decision problem
- 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)\)
- Solving non-linear arithmetic
- Splitting on Demand in SAT Modulo Theories
- Term Rewriting and All That
- The MathSAT5 SMT solver
- Theorem proving using lazy proof explication.
- Theory Instantiation
- Theory and Applications of Satisfiability Testing
- 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
- dReal: an SMT solver for nonlinear theories over the reals
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(only showing first 100 items - show all)- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- SMT-based and fixed-point approaches for state estimation in max-plus linear systems
- 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
- Multi-dimensional interpretations for termination of term rewriting
- Interpolation and model checking for nonlinear arithmetic
- Quantifier simplification by unification in SMT
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Virtual substitution for SMT-solving
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Computer Aided Verification
- Separation logics and modalities: a survey
- Taking satisfiability to the next level with Z3 (abstract)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- SMC: satisfiability modulo convex optimization
- Closure certificates
- Unbounded procedure summaries from bounded environments
- Designing theory solvers with extensions
- Splitting on Demand in SAT Modulo Theories
- An experiment with satisfiability modulo SAT
- A solver for arrays with concatenation
- Combined Satisfiability Modulo Parametric Theories
- Truncating abstraction of bit-vector operations for BDD-based SMT solvers
- Extending ACL2 with SMT solvers
- An instantiation scheme for satisfiability modulo theories
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Interpolation and SAT-based model checking revisited: adoption to software verification
- A Practical Approach to Discretised PDDL+ Problems by Translation to Numeric Planning
- A Tutorial on Satisfiability Modulo Theories
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
- Reliable reconstruction of fine-grained proofs in a proof assistant
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- Congruence closure modulo groups
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Lazy satisfiability modulo theories
- Satisfiability modulo theories: an appetizer
- An SMT-based approach for verifying binarized neural networks
- Experiments on infinite model finding in SMT solving
- An interactive SMT tactic in Coq using abductive reasoning
- Towards finding longer proofs
- Reasoning about vectors: satisfiability modulo a theory of sequences
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Satisfiability modulo bounded checking
- Solving quantified verification conditions using satisfiability modulo theories
- SMT sampling via model-guided approximation
- A framework for satisfiability modulo theories
- Efficient detection of redundancies in systems of linear inequalities
- A bit-vector differential model for the modular addition by a constant
- Model learning as a satisfiability modulo theories problem
- scientific article; zbMATH DE number 6528599 (Why is no real title available?)
- Temporal logic and fair discrete systems
- Rocket-Fast Proof Checking for SMT Solvers
- Binary decision diagrams
- Satisfiability modulo transcendental functions via incremental linearization
- A modular approach to MaxSAT modulo theories
- A logic-based framework leveraging neural networks for studying the evolution of neurological disorders
- An Abstract Framework for Satisfiability Modulo Theories
- Symbolic pattern planning
- A Progressive Simplifier for Satisfiability Modulo Theories
- A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis
- Deciding local theory extensions via E-matching
- Instantiation of SMT problems modulo integers
- A practical approach to satisfiability modulo linear integer arithmetic
- Natural domain SMT: a preliminary assessment
- Verified verifying: SMT-LIB for strings in Isabelle
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Satisfiability checking: theory and applications
- MCMT: a model checker modulo theories
- Bugs, moles and skeletons: symbolic reasoning for software development
- Certainty in formalising SMT-LIB for strings in Isabelle
- SAT-Based Model Checking
- A survey of satisfiability modulo theory
- Solving constraint satisfaction problems with SAT modulo theories
- Computing inductive invariants of regular abstraction frameworks
- Politeness and stable infiniteness: stronger together
- Towards universally accessible SAT technology
- Modal Satisfiability via SMT Solving
- Risk-aware shielding of partially observable Monte Carlo planning policies
- SMT and functional equation solving over the reals: challenges from the IMO
- Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
- More is less: adding polynomials for faster explanations in NLSAT
- Local Search for SMT on Linear Integer Arithmetic
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Challenges in Satisfiability Modulo Theories
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- The problem of checking the satisfiability of formulae of decidable theories (survey)
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Adversarial reachability for program-level security analysis
- Closure certificates
- From Propositional Satisfiability to Satisfiability Modulo Theories
- On SAT Modulo Theories and Optimization Problems
- Combining Model Checking and Deduction
- Even Faster Conflicts and Lazier Reductions for String Solvers
- \textsf{TSAT++}: an open platform for satisfiability modulo theories
- Lessons on datasets and paradigms in machine learning for symbolic computation: a case study on CAD
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)
