基于活性编码的EUF公式的判定过程
A Decision Procedure of EUF Formulas Based on Eager Encoding
DOI: 10.12677/SEA.2020.91006, PDF,   
作者: 程梦奇, 雷斯然, 江建国*：辽宁师范大学数学学院，辽宁 大连
关键词: EUF公式；Ackermann归约；等式图；EUF Formula； Ackermann’s Reduction； Equality Graph
摘要: 在形式化验证领域，EUF公式的活性编码判定过程解决某些问题具有实际的优势，判定组合理论时，该方法选择将其归约为命题公式，更易于求解。本文以寻找高效的EUF公式的活性编码判定过程为目的，研究了一个活性编码方法，即通过Ackermann归约算法以及基于非极性等式图的归约算法，将EUF公式归约为等可满足性的命题公式。为了简化这一方法的实现进程，本文基于C++语言编写的DPLIB库，根据上述算法添加程序并成功编译于Linux系统，可以调用它更快的求解EUF公式。
Abstract: In the formal verification community, a decision procedure of EUF formulas based on eager encoding method has practical advantages in solving certain problems. It also promotes the option of deciding a combination of theories by reducing them to this logic. In this paper, in order to find an efficient decision procedure of EUF formulas based on eager encoding, an eager approach is studied that an EUF formula is reduced to propositional logic formula by Ackermann’s method and an algorithm based on a nonpolar equality graph. The DPLIB library written in C++ language is provided for simplifying the development of the procedure. After adding the code to implement the above algorithms and compiling it on Linux system, it can be called to solve an EUF formula faster.
文章引用：程梦奇, 雷斯然, 江建国. 基于活性编码的EUF公式的判定过程[J]. 软件工程与应用, 2020, 9(1): 49-55. https://doi.org/10.12677/SEA.2020.91006

参考文献

[1] Kroening, D. and Strichman, O. (2016) Equality Logic and Uninterpreted Functions. In: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, Springer, Berlin, 77-95. [Google Scholar] [CrossRef] 
[2] Lei, B.U. and Bao, X.D. (2014) Formal Verification of Hybrid System. Journal of Software, 25, 219-233.
[3] Bryant, R.E., German, S. and Velev, M.N. (2001) Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. ACM Transactions on Computational Logic, 2, 1-41. [Google Scholar] [CrossRef] 
[4] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A. and Peled, D. (2004) DPLL(T): Fast Decision Procedures. In: Alur, R. and Peled, D.A., Eds., Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, Volume 3114, Springer, Berlin, Heidelberg, 175-188. [Google Scholar] [CrossRef] 
[5] 金继伟, 马菲菲, 张健. SMT求解技术简述[J]. 计算机科学与探索, 2015, 9(7): 769-780.
[6] Seshia, S.A., Lahiri, S.K. and Bryant, R.E. (2003) A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions. In: Proceedings of the 40th Annual Design Automation Conference, ACM, New York, 425-430. [Google Scholar] [CrossRef] 
[7] Pnueli, A., Rodeh, Y. and Shtrichman, O. (1999) Deciding Equality Formulas by Small Domains Instantiations. In: Halbwachs, N. and Peled, D., Eds., Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, Volume 1633, Springer, Berlin, Heidelberg, 455-469. [Google Scholar] [CrossRef] 
[8] 王翀, 吕荫润, 陈力, 王秀利, 王永吉. SMT求解技术的发展及最新应用研究综述[J]. 计算机研究与发展, 2017, 54(7): 1405-1425.
[9] Kroening, D. and Strichman, O. (2009) A Framework for Satisfiability Modulo Theories. Formal Aspects of Computing, 21, 485-494. [Google Scholar] [CrossRef] 
[10] Strichman, O. (2002) On Solving Presburger and Linear Arithmetic with SAT. In: Aagaard, M.D. and O’Leary, J.W., Eds., Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, Volume 2517, Springer, Berlin, Heidelberg, 160-170. [Google Scholar] [CrossRef] 
[11] Bryant, R.E., German, S. and Velev, M.N. (1999) Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. In: Halbwachs, N. and Peled, D., Eds., Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, Volume 1633, Springer, Berlin, Heidelberg, 470-482. [Google Scholar] [CrossRef] 
[12] Pnueli, A. and Strichman, O. (2006) Reduced Functional Consistency of Uninterpreted Functions. Electronic Notes in Computer Science, 144, 53-65. [Google Scholar] [CrossRef] 
[13] Rodeh, Y. and Shtrichman, O. (2001) Finite Instantiations in Equivalence Logic with Uninterpreted Functions. In: Berry, G., Comon, H. and Finkel, A., Eds., Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, Volume 2102. Springer, Berlin, Heidelberg, 144-154. [Google Scholar] [CrossRef] 
[14] Rodeh, Y. and Strichman, O. (2006) Building Small Equality Graphs for Deciding Equality Logic with Uninterpreted Functions. Information and Computation, 204, 26-59. [Google Scholar] [CrossRef] 
[15] Bryant, R.E. and Velev, M.N. (2002) Boolean Satisfiability with Transitivity Constraints. ACM Transactions on Computational Logic, 3, 604-627. [Google Scholar] [CrossRef] 

为你推荐