Satisfiability Modulo Theories
From MaRDI portal
Publication:3176369
DOI10.1007/978-3-319-10575-8_11zbMath1392.68379OpenAlexW1481397690MaRDI QIDQ3176369
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_11
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (36)
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Quantifier simplification by unification in SMT ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Temporal Logic and Fair Discrete Systems ⋮ Binary Decision Diagrams ⋮ SAT-Based Model Checking ⋮ Combining Model Checking and Deduction ⋮ 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 ⋮ Separation logics and modalities: a survey ⋮ 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 ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ A bit-vector differential model for the modular addition by a constant ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks* ⋮ An SMT-based approach for verifying binarized neural networks ⋮ Unbounded procedure summaries from bounded environments ⋮ 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 ⋮ 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 ⋮ 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 ⋮ A Practical Approach to Discretised PDDL+ Problems by Translation to Numeric Planning
Uses Software
Cites Work
- Combined Satisfiability Modulo Parametric Theories
- Verification, Model Checking, and Abstract Interpretation
- Model Checking Software
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal Methods at the Crossroads. From Panacea to Foundational Support
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Bounded model checking using satisfiability solving
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An instantiation scheme for satisfiability modulo theories
- Resolution proof transformation for compression and interpolation
- Model-theoretic methods in combined constraint satisfiability
- Constraint solving for interpolation
- Combining nonstably infinite theories
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Fast congruence closure and extensions
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Complexity, convexity and combinations of theories
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Efficient theory combination via Boolean search
- SMT proof checking using a logical framework
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- An interpolating theorem prover
- Solvable cases of the decision problem
- Model-based Theory Combination
- Solving Non-linear Arithmetic
- An Abstract Interpretation of DPLL(T)
- Efficient generation of craig interpolants in satisfiability modulo theories
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
- BDD-Based Symbolic Model Checking
- SAT-Based Model Checking
- Interpolation and Model Checking
- Predicate Abstraction for Program Verification
- Conflict Resolution
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- A Compressing Translation from Propositional Resolution to Natural Deduction
- Towards SMT Model Checking of Array-Based Systems
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Ground Interpolation for the Theory of Equality
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Generalizing DPLL to Richer Logics
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Variations on the Common Subexpression Problem
- Efficiency of a Good But Not Linear Set Union Algorithm
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Negative-cycle detection algorithms
- Term Rewriting and All That
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
- More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
- Polite Theories Revisited
- Ground Interpolation for Combined Theories
- A comprehensive combination framework
- Computer Aided Verification
- The MathSAT5 SMT Solver
- Proof Tree Preserving Interpolation
- Theory Instantiation
- Splitting on Demand in SAT Modulo Theories
- Logics in Artificial Intelligence
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- A Decision Procedure for Bit-Vectors and Arrays
- Decision Procedures for Multisets with Cardinality Constraints
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Rocket-Fast Proof Checking for SMT Solvers
- Frontiers of Combining Systems
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Mechanizing Mathematical Reasoning
- Boolean satisfiability with transitivity constraints
- Fast LCF-Style Proof Reconstruction for Z3
- MCMT: A Model Checker Modulo Theories
- On SAT Modulo Theories and Optimization Problems
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- A Reachability Predicate for Analyzing Low-Level Software
- Deciding Bit-Vector Arithmetic with Abstraction
This page was built for publication: Satisfiability Modulo Theories
