A Unified Framework for DPLL(T) + Certificates
Joint Authors
Wang, Bow-Yaw
Gu, Ming
Sun, Jiaguang
Zhou, Min
He, Fei
Source
Journal of Applied Mathematics
Issue
Vol. 2013, Issue 2013 (31 Dec. 2013), pp.1-13, 13 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2013-05-23
Country of Publication
Egypt
No. of Pages
13
Main Subjects
Abstract EN
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.
American Psychological Association (APA)
Zhou, Min& He, Fei& Wang, Bow-Yaw& Gu, Ming& Sun, Jiaguang. 2013. A Unified Framework for DPLL(T) + Certificates. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-13.
https://search.emarefa.net/detail/BIM-511970
Modern Language Association (MLA)
Zhou, Min…[et al.]. A Unified Framework for DPLL(T) + Certificates. Journal of Applied Mathematics No. 2013 (2013), pp.1-13.
https://search.emarefa.net/detail/BIM-511970
American Medical Association (AMA)
Zhou, Min& He, Fei& Wang, Bow-Yaw& Gu, Ming& Sun, Jiaguang. A Unified Framework for DPLL(T) + Certificates. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-13.
https://search.emarefa.net/detail/BIM-511970
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-511970