Verification by approximate forward and backward reachability

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verification by approximate forward and backward reachability

Full text

Pdf (617 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design table of contents

San Jose, California, United States

Pages: 366 - 370

Year of Publication: 1998

ISBN:1-58113-008-2

Authors

Shankar G. Govindaraju	Computer Systems Laboratory, Stanford University, Stanford, CA
David L. Dill	Computer Systems Laboratory, Stanford University, Stanford, CA

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society
IEEE-EDS : Electronic Devices Society
IEEE-CAS : Circuits & Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 17, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/288548.289055 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	2	Burch, J. R., Clarke, E. M., McMiHan, K. L., Dill, D, L, and I-hvang, L. J., "Symbolic Model Checking: 1020 States and Beyond," LICS 1990, pp. 428-439.
	3	Gianpiero Cabodi , P. Camurati , Stefano Quer, Symbolic exploration of large circuits with enhanced forward/backward traversals, Proceedings of the conference on European design automation, p.22-27, September 19-23, 1994, Grenoble, France
	4	Cho, H. et. aI, "Algorithms for Approximate FSM Traversal Based on State Space Decomposition," FEEE TCAD, Vol. 15, No. 12, pp. 1465-1478, December 1996.
	5	David L. Dill , Howard Wong-Toi, Verification of Real-Time Systems by Successive Over and Under Approximation, Proceedings of the 7th International Conference on Computer Aided Verification, p.409-422, July 03-05, 1995
	6	Thomas Filkorn, Functional Extension of Symbolic Model Checking, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.225-232, July 01-04, 1991
	7	Shankar G. Govindaraju , David L. Dill , Alan J. Hu , Mark A. Horowitz, Approximate reachability with BDDs using overlapping projections, Proceedings of the 35th annual conference on Design automation, p.451-456, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277169]
	8	J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
	9	Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
	10	Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
	11	Kavita Ravi , Kenneth L. McMillan , Thomas R. Shiple , Fabio Somenzi, Approximation and decomposition of binary decision diagrams, Proceedings of the 35th annual conference on Design automation, p.445-450, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277168]

CITED BY 6

	Shankar G. Govindaraju , David L. Dill , Jules P. Bergmann, Improved approximate reachability using auxiliary state variables, Proceedings of the 36th ACM/IEEE conference on Design automation, p.312-316, June 21-25, 1999, New Orleans, Louisiana, United States
	Shankar G. Govindaraju , David L. Dill, Counterexample-guided choice of projections in approximate symbolic model checking, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
	Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003
	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Can BDDs compete with SAT solvers on bounded model checking?, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proceedings of the conference on Design, Automation and Test in Europe, p.10898, March 03-07, 2003
	Sharon Shoham , Orna Grumberg, A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.1-es, December 2007