A Unified Framework for DPLL(T) + Certificates. (23rd May 2013)
- Record Type:
- Journal Article
- Title:
- A Unified Framework for DPLL(T) + Certificates. (23rd May 2013)
- Main Title:
- A Unified Framework for DPLL(T) + Certificates
- Authors:
- Zhou, Min
He, Fei
Wang, Bow-Yaw
Gu, Ming
Sun, Jiaguang - Other Names:
- Song Xiaoyu Academic Editor.
- Abstract:
- Abstract : 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.
- Is Part Of:
- Journal of applied mathematics. Volume 2013(2013)
- Journal:
- Journal of applied mathematics
- Issue:
- Volume 2013(2013)
- Issue Display:
- Volume 2013, Issue 2013 (2013)
- Year:
- 2013
- Volume:
- 2013
- Issue:
- 2013
- Issue Sort Value:
- 2013-2013-2013-0000
- Page Start:
- Page End:
- Publication Date:
- 2013-05-23
- Subjects:
- Mathematics -- Periodicals
519.05 - Journal URLs:
- https://www.hindawi.com/journals/jam/ ↗
- DOI:
- 10.1155/2013/964682 ↗
- Languages:
- English
- ISSNs:
- 1110-757X
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library HMNTS - ELD Digital store
- Ingest File:
- 17023.xml