[1]
|
Craig, W. (1957) Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. The Journal of Symbolic Logic, 22, 269-285. http://dx.doi.org/10.2307/2963594
|
[2]
|
McMillan, K.L. (2003) Interpolation and SAT-Based Model Checking. In: CAV 2003: 2003 Proceedings of the 15th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer, Berlin, 1-13.
|
[3]
|
Weissenbacher, G. (2010) Program Analysis with Interpolants. Magdalen College, Oxford University, Oxford, England, 277.
|
[4]
|
Henzinger, T.A., Jhala, R., Majumdar, R., et al. (2004) Abstractions from Proofs. ACM SIGPLAN Notices, 39, 232- 244.
|
[5]
|
Bruttomesso, R., Rollini, S.F., Sharygina, N., et al. (2010) Flexible Interpolation Generation in Satisfiability Modulo Theories. ICCAD 2010: 2010 Proceedings of the 14th International Conference on Computer-Aided Design, IEEE, Piscataway, 770-777.
|
[6]
|
陈祖希, 徐中伟, 霍伟伟, 等. 基于Craig插值的线性混成系统符号化模型检测[J]. 电子学报, 2014(7): 1338- 1346.
|
[7]
|
McMillan, K.L., Ball, T. and Jones, R.B. (2006) Lazy Abstraction with Interpolations. In: CAV 2006: 2006 Proceedings of the 18th Conference on Computer Aided Verification, Springer, Berlin, 123-136.
|
[8]
|
屈婉霞, 李暾, 郭阳, 杨晓东. 模型检验中抽象技术研究综述[J]. 计算机工程与应用, 2006, 42(33): 15-19.
|
[9]
|
Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2006) Solving SAT and SAT Modulo Theories: From an Abstract Davis- Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 53, 937-977.
|
[10]
|
Pudlak, P. (1997) Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Mathematical Institute Academy of Sciences of Czech Republic, 62, 1-20. http://dx.doi.org/10.2307/2275583
|
[11]
|
Alberti, F., et al. (2014) An Extension of Lazy Abstraction with Interpolation of Programs with Arrays. Formal Methods in System Design, 45, 63-109. http://dx.doi.org/10.1007/s10703-014-0209-9
|
[12]
|
Lopes, N.P. and Monteiro, J. (2015) Automatic Equivalence Checking of Programs with Uninterpreted Functions and Integer Arithmetic. International Journal on Software Tools for Technology Transfer, Springer, Science, 1-16.
|
[13]
|
Fitting, M. (1996) First-Order Logic and Automated Theorem Proving. Springer, Berlin.
http://dx.doi.org/10.1007/978-1-4612-2360-3
|