Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification

作者: Deepak Kapur

DOI: 10.1007/BFB0028393

关键词:

摘要:

参考文章(14)
Harald Rueß, Natarajan Shankar, Mandayam K Srivas, Modular Verification of SRT Division computer aided verification. pp. 123- 134 ,(1996) , 10.1007/3-540-61474-5_63
Hantao Zhang, Implementing Contextual Rewriting CTRS '92 Proceedings of the Third International Workshop on Conditional Term Rewriting Systems. pp. 363- 377 ,(1992) , 10.1007/3-540-56393-8_28
Deepak Kapur, Shostak's congruence closure as completion Rewriting Techniques and Applications. pp. 23- 37 ,(1997) , 10.1007/3-540-62950-5_59
Hantao Zhang, Deepak Kapur, Mukkai S Krishnamoorthy, A Mechanizable Induction Principle for Equational Specifications conference on automated deduction. pp. 162- 181 ,(1988) , 10.1007/BFB0012831
Randal E. Bryant, Yirng-An Chen, Verification of Arithmetic Functions with Binary Moment Diagrams Carnegie Mellon University. ,(1994) , 10.21236/ADA281028
Deepak Kapur, M. Subramaniam, New Uses of Linear Arithmetic in Automated Theorem Proving by Induction Journal of Automated Reasoning. ,vol. 16, pp. 39- 78 ,(1995) , 10.1007/BF00244459
Robert E. Shostak, Deciding Combinations of Theories Journal of the ACM. ,vol. 31, pp. 1- 12 ,(1984) , 10.1145/2422.322411
D. Kapur, H. Zhang, An overview of Rewrite Rule Laboratory (RRL) Computers & Mathematics with Applications. ,vol. 29, pp. 91- 114 ,(1995) , 10.1016/0898-1221(94)00218-A
Bryant, Graph-Based Algorithms for Boolean Function Manipulation IEEE Transactions on Computers. ,vol. 35, pp. 677- 691 ,(1986) , 10.1109/TC.1986.1676819
J. Strother Moore, Robert S. Boyer, A Computational Logic Handbook ,(1988)