This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.S. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
R.E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE trans. on Computers, C-35(8), 1986.
R. E. Bryant, and Y.-A. Chen, “Verification of arithmetic functions with binary moment diagrams,” Tech. Rep. CMU-CS-94-160, June 1994.
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.
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.
D. Kapur, “Shostak's congruence closure as completion,” Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA-97), Barcelona, Spain, June 1997.
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.
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.
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.
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.
D. Kapur and M. Subramaniam, “Intermediate lemma generation from circuit descriptions,” under preparation, State University of New York, Albany, NY, May 1997.
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.
D. Kapur, and H. Zhang, “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 1995, 91–114.
G. Nelson, and D.C. Oppen, “Simplification by cooperating decision procedures,” ACM Tran. on Programming Languages and Systems 1 (2), 1979, 245–257.
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.
R.E. Shostak, “Deciding combination of theories,” Journal of ACM 31 (1), 1984, 1–12.
H. Zhang, “Implementing contextual rewriting,” Proc. 3rd Intl. Workshop on Conditional Term Rewriting Systems, Springer LNCS 656, (eds. Remy and Rusinowitch), 1992, 363–377.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D. (1997). Rewriting, decision procedures and lemma speculation for automated hardware verification. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028393
Download citation
DOI: https://doi.org/10.1007/BFb0028393
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63379-2
Online ISBN: 978-3-540-69526-4
eBook Packages: Springer Book Archive