Combining Decision Procedures by (Model-)Equality Propagation

DOI10.1016/j.entcs.2009.05.048zbMath1347.68309OpenAlexW1994641146MaRDI QIDQ5179357

David Déharbe, Pascal Fontaine, Diego Caminha B. de Oliveira

Publication date: 19 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.048

zbMATH Keywords

automatic theorem provingSMT solverscombination of decision procedures

Mathematics Subject Classification ID

Related Items (1)

Combining decision procedures by (model-)equality propagation

Uses Software

• Coq
• ML
• Isabelle/HOL
• z3
• HOL
• HOL Light

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Isabelle/HOL. A proof assistant for higher-order logic
• Formal methods in computer-aided design. 1st international conference, FMCAD '96, Palo Alto, CA, USA, November 6--8, 1996. Proceedings
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• Model-based Theory Combination
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• The B-Book
• Splitting on Demand in SAT Modulo Theories
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Frontiers of Combining Systems
• Computer Aided Verification

This page was built for publication: Combining Decision Procedures by (Model-)Equality Propagation