Efficient theory combination via Boolean search
From MaRDI portal
Publication:2432765
Recommendations
Cites work
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Combining non-stably infinite theories
- Complexity, convexity and combinations of theories
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Congruence closure with integer offsets
- Deciding Combinations of Theories
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1140674 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1979549 (Why is no real title available?)
- scientific article; zbMATH DE number 1798183 (Why is no real title available?)
- scientific article; zbMATH DE number 2086594 (Why is no real title available?)
- scientific article; zbMATH DE number 2086596 (Why is no real title available?)
- scientific article; zbMATH DE number 1903355 (Why is no real title available?)
- scientific article; zbMATH DE number 2090060 (Why is no real title available?)
- Simplification by Cooperating Decision Procedures
- Solvable cases of the decision problem
- Theorem proving using lazy proof explication.
- Theoretical Aspects of Computing - ICTAC 2004
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
- Unions of non-disjoint theories and combinations of satisfiability procedures
Cited in
(22)- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Theory decision by decomposition
- Combination of convex theories: modularity, deduction completeness, and explanation
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Being careful about theory combination
- Decision procedures for extensions of the theory of arrays
- Model-based theory combination
- Optimization modulo theories with linear rational costs
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Sharing is caring: combination of theories
- Satisfiability modulo theories
- Verifying Heap-Manipulating Programs in an SMT Framework
- Towards SMT Model Checking of Array-Based Systems
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Combining equational reasoning
- Combining decision procedures by (model-)equality propagation
- Solving constraint satisfaction problems with SAT modulo theories
- Ground Interpolation for Combined Theories
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Exploiting partial-assignment enumeration in optimization modulo theories
This page was built for publication: Efficient theory combination via Boolean search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2432765)
