Automatic compositional minimization in CTL model checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Automatic compositional minimization in CTL model checking

Full text

Pdf (843 KB)

Source

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

Santa Clara, California, United States

Pages: 172 - 178

Year of Publication: 1992

ISBN:0-89791-540-2

Authors

Massimiliano Chiodo	Magneti Marelli, Pavia, Italy
Thomas R. Shiple	Department of EECS, University of California, Berkeley, CA
Alberto L. Sangiovanni-Vincentelli	Department of EECS, University of California, Berkeley, CA
Robert K. Brayton	Department of EECS, University of California, Berkeley, CA

Sponsors

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

Publisher

IEEE Computer Society Press Los Alamitos, CA, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 7, Citation Count: 5

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

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	D. Arnett, "A High Performance Solution for In-Vehicle Networking - 'Controller Area Network (CAN),"' SAE Technical Paper Series, 870823, Apr. 1987.
	2	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]
	3	J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
	4	J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127702]
	5	M. Chiodo, T. R. Shiple, A. Sangiovanni-Vincentelli, and R. K. Brayton, "Automatic Reduction in CTL Compositional Model Checking," Memorandum No. UCB/ERL M92/55, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, Jan. 1992.
	6	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]
	7	E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
	8	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
	9	O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
	10	E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	11	Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
	12	Orna Grumberg , David E. Long, Model Checking and Modular Verification, Proceedings of the 2nd International Conference on Concurrency Theory, p.250-265, August 26-29, 1991
	13	J. E. Hopcroft, "An n log n Algorithm for Minimizing the States in a Finite Automaton," in The Theory of Machines and Computation, New York: Academic Press, pp. 189-196, 1971.
	14	R. P. Kurshan , K. McMillan, A structural induction theorem for processes, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.239-247, June 1989, Edmonton, Alberta, Canada [doi>10.1145/72981.72998]
	15	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
	16	Z. Manna and A. Pneuli, "Verification of Concurrent Programs: The Temporal Framework," in The Correctness Problem in Computer Science, editors R. S. Boyer and J. Strother Moore, Int. Lecture Series in Computer Science, London: Academic Press, pp. 215-273, 1981.
	17	Ellen Sentovich , Kanwar Jit Singh , Cho W. Moon , Hamid Savoj , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Sequential Circuit Design Using Synthesis and Optimization, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.328-333, October 11-14, 1992
	18	H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. S angiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines using BDDs," in Proc. oflEEE International Conference on Computer-Aided Design, pp. 130-133, Nov. 1990.
	19	P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France

CITED BY 5

	Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Alan J. Hu , Gary York , David L. Dill, New techniques for efficient verification with implicitly conjoined BDDs, Proceedings of the 31st annual conference on Design automation, p.276-282, June 06-10, 1994, San Diego, California, United States
	Alberto L. Sangiovanni-Vincentelli , Patrick C. McGeer , Alexander Saldanha, Verification of electronic systems, Proceedings of the 33rd annual conference on Design automation, p.106-111, June 03-07, 1996, Las Vegas, Nevada, United States
	Adnan Aziz , Thomas Shiple , Vigyan Singhal , Robert Brayton , Alberto Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking, Formal Methods in System Design, v.21 n.2, p.193-224, September 2002