Rewriting, decision procedures and lemma speculation for automated hardware verification

1. R.S. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.

   Google Scholar 

2. R.E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE trans. on Computers, C-35(8), 1986.

   Google Scholar 

3. R. E. Bryant, and Y.-A. Chen, “Verification of arithmetic functions with binary moment diagrams,” Tech. Rep. CMU-CS-94-160, June 1994.

   Google Scholar 

4. J. R. Burch, E.M. Clarke, K. L. Mcmillan and D.L. Dill, “Sequential circuit verification using symbolic model checking,” Proc. 27th ACM/IEEE Design Automation Conference, 1990.

   Google Scholar 

5. E.M. Clarke, S.M. German and X. Zhao, “Verifying the SRT division algorithm using theorem proving techniques,” Proc. Computer Aided Verification, 8th Intl. Conf.-CAV'96, New Brunswick, July/August 1996, Springer LNCS 1102 (eds. Alur and Henzinger), 111–122.

   Google Scholar 

6. D. Kapur, “Shostak's congruence closure as completion,” Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA-97), Barcelona, Spain, June 1997.

   Google Scholar 

7. D. Kapur and X. Nie, “Reasoning about numbers in Tecton,” Proc. 8th Intl. Symp. Methodologies for Intelligent Systems, (ISMIS'94), Charlotte, North Carolina, October 1994, 57–70.

   Google Scholar 

8. D. Kapur and M. Subramaniam, “New uses of linear arithmetic in automated theorem proving for induction,” J. Automated Reasoning, 16(1–2), 1996, 39–78.

   Google Scholar 

9. D. Kapur and M. Subramaniam, “Mechanically verifying a family of multiplier circuits,” Proc. Computer Aided Verification (CA V96), New Jersey, Springer LNCS 1102 (eds. Alur and Henzinger), 1996, 135–146.

   Google Scholar 

10. D. Kapur and M. Subramaniam, “Mechanical verification of adder circuits using powerlists,” Dept. of Computer Science Tech. Report, SUNY Albany, November 1995. Accepted for publication in J. of Formal Methods in System Design.

    Google Scholar 

11. D. Kapur and M. Subramaniam, “Intermediate lemma generation from circuit descriptions,” under preparation, State University of New York, Albany, NY, May 1997.

    Google Scholar 

12. D. Kapur and M. Subramaniam, “An automatic proof of properties of an SRT division circuit,” under preparation, State University of New York, Albany, NY, May 1997.

    Google Scholar 

13. D. Kapur, and H. Zhang, “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 1995, 91–114.

    Google Scholar 

14. G. Nelson, and D.C. Oppen, “Simplification by cooperating decision procedures,” ACM Tran. on Programming Languages and Systems 1 (2), 1979, 245–257.

    Google Scholar 

15. H. Ruess, N. Shankar and M.K. Srivas, “Modular verification of SRT division,” Proc. Computer Aided Verification, 8th Intl. Conf. — CAV'96, New Brunswick, July/August 1996, Springer LNCS 1102 (eds. Alur and Henzinger), 123–134.

    Google Scholar 

16. R.E. Shostak, “Deciding combination of theories,” Journal of ACM 31 (1), 1984, 1–12.

    Google Scholar 

17. H. Zhang, “Implementing contextual rewriting,” Proc. 3rd Intl. Workshop on Conditional Term Rewriting Systems, Springer LNCS 656, (eds. Remy and Rusinowitch), 1992, 363–377.

    Google Scholar 

18. H. Zhang, D. Kapur, and M.S. Krishnamoorthy, “A mechanizable induction principle for equational specifications,” Proc. 9th Intl. Conf. Automated Deduction (CADE), Springer LNCS 310, (eds. Lusk and Overbeek), Chicago, 1988, 250–265.

    Google Scholar 

Download references