A Unified Framework for DPLL(T) + Certificates
المؤلفون المشاركون
Wang, Bow-Yaw
Gu, Ming
Sun, Jiaguang
Zhou, Min
He, Fei
المصدر
Journal of Applied Mathematics
العدد
المجلد 2013، العدد 2013 (31 ديسمبر/كانون الأول 2013)، ص ص. 1-13، 13ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2013-05-23
دولة النشر
مصر
عدد الصفحات
13
التخصصات الرئيسية
الملخص 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.
نمط استشهاد جمعية علماء النفس الأمريكية (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
نمط استشهاد الجمعية الأمريكية للغات الحديثة (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
نمط استشهاد الجمعية الطبية الأمريكية (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
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-511970
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر