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...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/964682 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832553747908132864 |
|---|---|
| author | Min Zhou Fei He Bow-Yaw Wang Ming Gu Jiaguang Sun |
| author_facet | Min Zhou Fei He Bow-Yaw Wang Ming Gu Jiaguang Sun |
| author_sort | Min Zhou |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-5ea5e2fc47404baba886c9233c0ec428 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-5ea5e2fc47404baba886c9233c0ec4282025-02-03T05:53:24ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/964682964682A Unified Framework for DPLL(T) + CertificatesMin Zhou0Fei He1Bow-Yaw Wang2Ming Gu3Jiaguang Sun4Tsinghua National Laboratory for Information Science and Technology (TNList), Beijing 100084, ChinaTsinghua National Laboratory for Information Science and Technology (TNList), Beijing 100084, ChinaInstitute of Information Science, Academia Sinica, Taipei 115, TaiwanTsinghua National Laboratory for Information Science and Technology (TNList), Beijing 100084, ChinaTsinghua National Laboratory for Information Science and Technology (TNList), Beijing 100084, ChinaSatisfiability 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.http://dx.doi.org/10.1155/2013/964682 |
| spellingShingle | Min Zhou Fei He Bow-Yaw Wang Ming Gu Jiaguang Sun A Unified Framework for DPLL(T) + Certificates Journal of Applied Mathematics |
| title | A Unified Framework for DPLL(T) + Certificates |
| title_full | A Unified Framework for DPLL(T) + Certificates |
| title_fullStr | A Unified Framework for DPLL(T) + Certificates |
| title_full_unstemmed | A Unified Framework for DPLL(T) + Certificates |
| title_short | A Unified Framework for DPLL(T) + Certificates |
| title_sort | unified framework for dpll t certificates |
| url | http://dx.doi.org/10.1155/2013/964682 |
| work_keys_str_mv | AT minzhou aunifiedframeworkfordplltcertificates AT feihe aunifiedframeworkfordplltcertificates AT bowyawwang aunifiedframeworkfordplltcertificates AT minggu aunifiedframeworkfordplltcertificates AT jiaguangsun aunifiedframeworkfordplltcertificates AT minzhou unifiedframeworkfordplltcertificates AT feihe unifiedframeworkfordplltcertificates AT bowyawwang unifiedframeworkfordplltcertificates AT minggu unifiedframeworkfordplltcertificates AT jiaguangsun unifiedframeworkfordplltcertificates |