A Unified Framework for DPLL(T) + Certificates

Satisfiability Modulo Theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based...

Full description

Bibliographic Details
Main Authors: Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun
Format: Article
Language:English
Published: Hindawi Limited 2013-01-01
Series:Journal of Applied Mathematics
Online Access:http://dx.doi.org/10.1155/2013/964682