|
|
|
|
A unified framework for DPLL(T) + certificates
|
|
|
|
|
|
|
|
نویسنده
|
zhou m. ,he f. ,wang b.-y. ,gu m. ,sun j.
|
|
منبع
|
journal of applied mathematics - 2013 - دوره : 2013 - شماره : 0
|
|
چکیده
|
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. © 2013 min zhou et al.
|
|
|
|
|
آدرس
|
tsinghua national laboratory for information science and technology (tnlist),beijing 100084,china,school of software,tsinghua university,beijing 100084,china,key laboratory for information system security,moe,beijing 100084,china,department of computer science and technologies,tsinghua university, China, tsinghua national laboratory for information science and technology (tnlist),beijing 100084,china,school of software,tsinghua university,beijing 100084,china,key laboratory for information system security,moe, China, institute of information science,academia sinica, Taiwan, tsinghua national laboratory for information science and technology (tnlist),beijing 100084,china,school of software,tsinghua university,beijing 100084,china,key laboratory for information system security,moe, China, tsinghua national laboratory for information science and technology (tnlist),beijing 100084,china,school of software,tsinghua university,beijing 100084,china,key laboratory for information system security,moe, China
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Authors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|