Formal verification in a commercial setting

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal verification in a commercial setting

Full text

Pdf (177 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 34th annual Design Automation Conference table of contents

Anaheim, California, United States

Pages: 258 - 262

Year of Publication: 1997

ISBN:0-89791-920-3

Author

R. P. Kurshan

Bell Laboratories, Murray Hill, NJ

Sponsors

EDAC : Electronic Design Automation Consortium
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

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

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/266021.266089 What is a DOI?

ABSTRACT

This tutorial addresses the following questions:¿ why do formal verification?¿ who is doing it today?¿ what are they doing?¿ how are they doing it?¿ what about the future?

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	Rajeev Alur , Robert P. Kurshan, Timing analysis in COSPAN, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.220-231, July 1996, New Brunswick, NeW Jersey, United States
	2	Bishop Brock , Matt Kaufmann , J. Strother Moore, ACL2 Theorems About Commercial Microprocessors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.275-293, November 06-08, 1996
	3	J.R. Burch, E. M. Clarke, D. Long, K. L. McMillan, D. L. Dill, Symbolic Model Checking for Sequential Circuit Verification, IEEE Trans. Computer Aided Design, 13 (1994) 401-424.
	4	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	5	Edmund M. Clarke , Robert P. Kurshan, Computer-aided verification, IEEE Spectrum, v.33 n.6, p.61-67, June 1996 [doi>10.1109/6.499951]
	6	R. H. Hardin, Z. Har'E1, R. P. Kurshan, COSPAN, Springer LNCS 1102 (1996) 423-427.
	7	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	8	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	9	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	10	http://dimacs.rutgers.edu/Workshops/SYLA- Tutorials/program.html

CITED BY 16

	Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States
	Constance Heitmeyer, Using SCR to specify requirements of the BART advanced automated train control system, High integrity software, Kluwer Academic Publishers, Norwell, MA, 2001
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	Constance Heitmeyer , James Kirby , Bruce Labaw, Applying the SCR requirements method to a weapons control panel: an experience report, Proceedings of the second workshop on Formal methods in software practice, p.92-102, March 04-05, 1998, Clearwater Beach, Florida, United States
	Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States
	Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States
	Leila Barakatain , Sofiène Tahar , Jean Lamarche , Jean-Marc Gendreau, Practical approaches to the verification of a telecom megacell using FormalCheck, Proceedings of the 11th Great Lakes symposium on VLSI, p.1-6, March 2001, West Lafayette, Indiana, United States
	R. Kurshan , V. Levin , M. Minea , D. Peled , H. Yenigün, Verifying hardware in its software context, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.742-749, November 09-13, 1997, San Jose, California, United States
	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
	Jan Van Katwijk , Ruud De Rooij , Sylvia Stuurman , Hans Toetenel, Software development and verification of dynamic real-time distributed systems based on the radio broadcast paradigm, Parallel and distributed real-time systems, Nova Science Publishers, Inc., Commack, NY, 2001
	Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
	Wenli Wang , Zoltán Hidvégi , Andrew D. Bailey , Andrew B. Whinston, E-Process Design and Assurance Using Model Checking, Computer, v.33 n.10, p.48-53, October 2000
	Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
	Yasushi Umezawa , Takeshi Shimizu, A Formal Verification Methodology for Checking Data Integrity, Proceedings of the conference on Design, Automation and Test in Europe, p.284-289, March 07-11, 2005
	Nabil El Kadhi , Hazem El-Gendy, Advanced method for cryptographic protocol verification, Journal of Computational Methods in Sciences and Engineering, v.6 n.5,6 Supplement 1, p.109-119, April 2006
	Moshe Y. Vardi, Automated verification: graphs, logic, and automata, Proceedings of the 18th international joint conference on Artificial intelligence, p.1603-1606, August 09-15, 2003, Acapulco, Mexico