Combining decision procedures by (model-)equality propagation
DOI10.1016/J.SCICO.2010.04.003zbMATH Open1243.68150OpenAlexW2043758997MaRDI QIDQ436376FDOQ436376
Authors: Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine 
Publication date: 20 July 2012
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.04.003
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- Title not available (Why is that?)
- Complexity, convexity and combinations of theories
- Isabelle/HOL. A proof assistant for higher-order logic
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- The existence of refinement mappings
- The B-Book
- Splitting on Demand in SAT Modulo Theories
- A machine program for theorem-proving
- Title not available (Why is that?)
- Computer Aided Verification
- Combining nonstably infinite theories
- Fast Decision Procedures Based on Congruence Closure
- Computing small clause normal forms
- Normal form transformations
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Combining non-stably infinite, non-first order theories
- Refactoring towards a layered architecture
- An efficient Nelson-Oppen decision procedure for difference constraints over rationals
- Model-based theory combination
- Deciding Combinations of Theories
- Title not available (Why is that?)
- Combining Decision Procedures by (Model-)Equality Propagation
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Frontiers of Combining Systems
- Tools and Algorithms for the Construction and Analysis of Systems
Cited In (7)
- Adapting real quantifier elimination methods for conflict set computation
- Title not available (Why is that?)
- Efficient theory combination via Boolean search
- Combining Decision Procedures by (Model-)Equality Propagation
- A general setting for flexibly combining and augmenting decision procedures
- Model-based theory combination
- Theories, solvers and static analysis by abstract interpretation
Uses Software
This page was built for publication: Combining decision procedures by (model-)equality propagation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q436376)
