Efficient theory combination via Boolean search
From MaRDI portal
Publication:2432765
DOI10.1016/J.IC.2005.05.011zbMATH Open1137.68578DBLPjournals/iandc/BozzanoBCJRRS06OpenAlexW2114037873WikidataQ62041344 ScholiaQ62041344MaRDI QIDQ2432765FDOQ2432765
Authors: Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani 
Publication date: 25 October 2006
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2005.05.011
Recommendations
Cites Work
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- Complexity, convexity and combinations of theories
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- Title not available (Why is that?)
- Theorem proving using lazy proof explication.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Deciding Combinations of Theories
- Title not available (Why is that?)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
- Solvable cases of the decision problem
- Computer Aided Verification
- Title not available (Why is that?)
- Combining non-stably infinite theories
- Theoretical Aspects of Computing - ICTAC 2004
- Computer Aided Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Congruence closure with integer offsets
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
Cited In (21)
- Decision procedures for extensions of the theory of arrays
- Verifying Heap-Manipulating Programs in an SMT Framework
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Being careful about theory combination
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Optimization modulo theories with linear rational costs
- Ground Interpolation for Combined Theories
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Combining decision procedures by (model-)equality propagation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Towards SMT Model Checking of Array-Based Systems
- Theory decision by decomposition
- Satisfiability modulo theories
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving constraint satisfaction problems with 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})$
- Combination of convex theories: modularity, deduction completeness, and explanation
- Sharing is caring: combination of theories
- Model-based theory combination
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Combining equational reasoning
Uses Software
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)
