A Unified Framework for DPLL(T) + Certificates | Zendy

Min Zhou | Zendy; Fei He | Zendy; Bow-Yaw Wang | Zendy; Ming Gu | Zendy; Jiaguang Sun | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Unified Framework for DPLL(T) + Certificates

Author(s) -

Min Zhou,

Fei He,

Bow-Yaw Wang,

Ming Gu,

Jiaguang Sun

Publication year - 2013

Publication title -

journal of applied mathematics

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.307

H-Index - 43

eISSN - 1687-0042

pISSN - 1110-757X

DOI - 10.1155/2013/964682

Subject(s) - computer science , dpll algorithm , soundness , correctness , certificate , programming language , satisfiability modulo theories , boolean satisfiability problem , simple (philosophy) , theoretical computer science , overhead (engineering) , algorithm , telecommunications , philosophy , phase locked loop , epistemology , jitter

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 on DPLL(T), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. The soundness and completeness for DPLL(T) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10%, which outperforms other methods, and the certificate checking procedure is quite time saving

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research