Combining decision procedures by (model-)equality propagation

DOI10.1016/j.scico.2010.04.003zbMath1243.68150OpenAlexW2043758997MaRDI QIDQ436376

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

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

zbMATH Keywords

formal verificationautomated theorem provingSMT solvingcombination of decision procedures

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Uses Software

• Coq
• MiniSat
• SMT-LIB
• z3
• HOL Light
• Chaff
• veriT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Combining nonstably infinite theories
• Complexity, convexity and combinations of theories
• Isabelle/HOL. A proof assistant for higher-order logic
• 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
• Combining Decision Procedures by (Model-)Equality Propagation
• Splitting on Demand in SAT Modulo Theories
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Frontiers of Combining Systems
• A machine program for theorem-proving
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems