Combining decision procedures by (model-)equality propagation

DOI10.1016/J.SCICO.2010.04.003MaRDI QIDQ436376zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

SMT solvingautomated theorem provingformal verificationcombination of decision procedures

Mathematics Subject Classification ID

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)

Recommendations

• Combining Decision Procedures by (Model-)Equality Propagation
• Computer Aided Verification
• Efficient theory combination via Boolean search
• Model-based theory combination
• Combining decision procedures.

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 2086596 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A machine program for theorem-proving
• An efficient Nelson-Oppen decision procedure for difference constraints over rationals
• Combining Decision Procedures by (Model-)Equality Propagation
• Combining non-stably infinite, non-first order theories
• Combining nonstably infinite theories
• Complexity, convexity and combinations of theories
• Computer Aided Verification
• Computing small clause normal forms
• Deciding Combinations of Theories
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Fast Decision Procedures Based on Congruence Closure
• Frontiers of Combining Systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Model-based theory combination
• Normal form transformations
• Refactoring towards a layered architecture
• Simplification by Cooperating Decision Procedures
• Splitting on Demand in SAT Modulo Theories
• The B-Book
• The existence of refinement mappings
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools

Cited in

(7)

• Adapting real quantifier elimination methods for conflict set computation
• Model-based theory combination
• scientific article; zbMATH DE number 2090084 (Why is no real title available?)
• Efficient theory combination via Boolean search
• Combining Decision Procedures by (Model-)Equality Propagation
• A general setting for flexibly combining and augmenting decision procedures
• Theories, solvers and static analysis by abstract interpretation

Describes a project that uses

Uses Software

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

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)