Efficient generation of counterexamples and witnesses in symbolic model checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Efficient generation of counterexamples and witnesses in symbolic model checking

Full text

Pdf (225 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 32nd annual ACM/IEEE Design Automation Conference table of contents

San Francisco, California, United States

Pages: 427 - 432

Year of Publication: 1995

ISBN:0-89791-725-1

Authors

E. M. Clarke	School of Computer Science, Carnegie Mellon University, Pittsburgh, PA
O. Grumberg	Computer Science Dept., The Technion, Haifa, 32000 Isreal
K. L. McMillan	Cadence Berkeley Labs., 1919 Addison Street, Ste. 303, Berkeley, CA
X. Zhao	School of Computer Science, Carnegie Mellon University, Pittsburgh, PA

Sponsors

EDAC : Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 50, Citation Count: 24

Additional Information:

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/217474.217565 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	J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
	3	E. M. Clarke , I. A. Browne , R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of &ohgr;-automata, Proceedings of the fifteenth colloquium on CAAP'90, p.103-116, May 1990, Copenhagen, Denmark
	4	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	5	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]
	6	D. L. Dill and E. M. Clarke. Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings, Part E 133(5), 1986.
	7	E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986.
	8	Z. Har'E1 and R. P. Kurshan. Software for analytical development of communications protocols. ATUT Technical Journal, 69(1):45-59, Jan.-Feb. 1990.
	9	Ramin Hojati , Robert K. Brayton , Robert P. Kurshan, BDD-Based Debugging Of Design Using Language Containment and Fair CTL, Proceedings of the 5th International Conference on Computer Aided Verification, p.41-58, June 28-July 01, 1993
	10	Ramin Hojati , Vigyan Singhal , Robert K. Brayton, Edge-Streett/ Edge-Rabin Automata Environment for, University of California at Berkeley, Berkeley, CA, 1994
	11	R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
	12	Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992
	13	C. L. Seitz. Ideas about arbiters. Lambda, 10(4), 1980.

CITED BY 24

	Scott Hazelhurst , Osnat Weissberg , Gila Kamhi , Limor Fix, A hybrid verification approach: getting deep into the design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Hiroaki Iwashita , Tsuneo Nakata, Forward model checking techniques oriented to buggy designs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.400-404, November 09-13, 1997, San Jose, California, United States
	Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001
	David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
	Yirng-An Chen , Fang-Sung Chen, Algorithms for compacting error traces, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Hyoung Seok Hong , Sung Deok Cha , Insup Lee , Oleg Sokolsky , Hasan Ural, Data flow testing as model checking, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Roderick Bloem , Harold N. Gabow , Fabio Somenzi, An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps, Formal Methods in System Design, v.28 n.1, p.37-56, January 2006
	Yonit Kesten , Amir Pnueli , Li-On Raviv , Elad Shahar, Model Checking with Strong Fairness, Formal Methods in System Design, v.28 n.1, p.57-84, January 2006
	I. Pill , S. Semprini , R. Cavada , M. Roveri , R. Bloem , A. Cimatti, Formal analysis of hardware requirements, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Franco Fummi , Graziano Pravadelli, Too Few or Too Many Properties? Measure it by ATPG!, Journal of Electronic Testing: Theory and Applications, v.23 n.5, p.373-388, October 2007
	Westley Weimer, Patches as better bug reports, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage metrics for temporal logic model checking, Formal Methods in System Design, v.28 n.3, p.189-212, May 2006
	Heon-Mo Koo , Prabhat Mishra, Functional test generation using property decompositions for validation of pipelined processors, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
	Duminda Wijesekera , Paul Ammann , Lingya Sun , Gordon Fraser, Relating counterexamples to test cases in CTL model checking specifications, Proceedings of the 3rd international workshop on Advances in model-based testing, p.75-84, July 09-12, 2007, London, United Kingdom
	Hana Chockler , Joseph Y. Halpern , Orna Kupferman, What causes a system to satisfy a specification?, ACM Transactions on Computational Logic (TOCL), v.9 n.3, p.1-26, June 2008
	Prabhat Mishra , Nikil Dutt, Specification-driven directed test generation for validation of pipelined processors, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.3, p.1-36, July 2008
	Nicola Bombieri , Franco Fummi , Graziano Pravadelli, Reuse and optimization of testbenches and properties in a TLM-to-RTL design flow, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.3, p.1-22, July 2008
	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
	Andrea Fedeli , Franco Fummi , Graziano Pravadelli, Properties Incompleteness Evaluation by Functional Verification, IEEE Transactions on Computers, v.56 n.4, p.528-544, April 2007
	Dave King , Trent Jaeger , Somesh Jha , Sanjit A. Seshia, Effective blame for information-flow violations, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
	Hana Chockler , Arie Gurfinkel , Ofer Strichman, Beyond vacuity: towards the strongest passing formula, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	Heon-Mo Koo , Prabhat Mishra, Functional test generation using design and property decomposition techniques, ACM Transactions on Embedded Computing Systems (TECS), v.8 n.4, p.1-33, July 2009