The complexity of verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The complexity of verification

Full text

Pdf (826 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the twenty-sixth annual ACM symposium on Theory of computing table of contents

Montreal, Quebec, Canada

Pages: 365 - 371

Year of Publication: 1994

ISBN:0-89791-663-8

Author

R. P. Kurshan

AT&T Bell Laboratories, Murray Hill, NJ

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/195058.195194 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	S. Aggarwal, R. E Kurshan, and K. Sabnani. A Calculus for Protocol Specification and Validation. In Protocol Specification, Testing and Verification iII, pages 19-34. North-I-tolland, 1993.
	2	B. Alpern and E B. Schneider. Defining Liveness. Inf. Proc. Letters 21, pages 181-185, (1985).
	3	B. Alpern and E B. Schneider. Recognizing Safety and Liveness. Distributed Computing 2, pages 117-126, (1987).
	4	Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
	5	Henrik Reif Andersen , Glynn Winskel, Compositional checking of satisfaction, Formal Methods in System Design, v.1 n.4, p.323-354, Dec. 1992 [doi>10.1007/BF00709155]
	6	C. M. Angelo , D. Verkest , L. Claesen , H. De Man, On the comparison of HOL and Boyer-Moore for formal hardware verification, Formal Methods in System Design, v.2 n.1, p.45-72, Feb. 1993 [doi>10.1007/BF01383943]
	7	G. Barnes, J. E Buss, W. L. Ruzzo, and B. Schieber. A Sublinear Space, Polynomial Time Algorithm for Directed s-t Connectivity. In Proc. 7th IEEE Structure in Complexity Thy. Conf., pages 27-33, (1992).
	8	J. Barwise. Mathematical Proofs of Computer System Correctness. Notices, Amer. Math. Soc. 36, pages 884- 851, (1989).
	9	W.W. Bledsoe and D. W. Loveland, editors. Automated Theorem Proving: After 25 Years, Contemp. Math 29. Amer. Math. Soc., 1984. Especially the paper "Proof- Checking, Theorem-Proving and Program Verification" by R. S. Boyer and J. S. Moore, 119-132.
	10	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]
	11	Y. Choueka. Theories of Automata on w-Tapes" A Simplified Approach. J. Comp. Sys. Sci. 8, pages 117- 141, (1974).
	12	E. M. Clarke , I. A. Draghicescu , R. P. Kurshan, A unified approach for showing language inclusion and equivalence between various types of &ohgr;-automata, Information Processing Letters, v.46 n.6, p.301-308, July 26, 1993 [doi>10.1016/0020-0190(93)90069-L]
	13	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
	14	E. M. Clarke , O. Grumberg , R. P. Kurshan, A synthesis of two approaches for verifying finite state concurrent systems, Logic at Botik'89 Symposium on logical foundations of computer science, Springer-Verlag New York, Inc., New York, NY, 1989
	15	A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
	16	C Courcoubetis , M Y Vardi , P Wolper, Reasoning about fair concurrent programs, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.283-294, May 28-30, 1986, Berkeley, California, United States [doi>10.1145/12130.12159]
	17	C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
	18	David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
	19	David L. Dill , Alan J. Hu , Howard Wong-Toi, Checking for Language Inclusion Using Simulation Preorders, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.255-265, July 01-04, 1991
	20	E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	21	Jean-Claude Fernandez , Laurent Mounier , Claude Jard , Thierry Jéron, On-the-fly verification of finite transition systems, Formal Methods in System Design, v.1 n.2-3, p.251-273, Oct. 1992 [doi>10.1007/BF00121127]
	22	M. R. Garey and D. S. Johnson. Computers and Intractability. Freeman, 1979.
	23	M. Gordon. A Proof-Generating System for Higher- Order Logic. Kluwer SECS 35, pages 73-128, (1988).
	24	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
	25	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
	26	Aarti Gupta, Formal hardware verification methods: a survey, Formal Methods in System Design, v.1 n.2-3, p.151-238, Oct. 1992 [doi>10.1007/BF00121125]
	27	Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
	28	Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
	29	Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
	30	J. Joyce. Formal Verification and Implementation of a Microprocessor. In G. B irtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 129-157. Kluwer Academic Press, Boston, 1988.
	31	Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
	32	D. Kozen. Lower Bounds for Natural Proof Systems. Proc 18th Symp. Found. Comput. Sci. (FOCS), pages 254-266, (1977).
	33	R. E Kurshan. Modelling Concurrent Processes. Symp. Applied Math. 31, pages 45-57, (1985).
	34	R. E Kurshan. Reducibility in Analysis of Coordination. LNCIS 103, pages 19-39, (1987).
	35	Robert P. Kurshan, Analysis of Discrete Event Coordination, Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, p.414-453, May 29-June 02, 1989
	36	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	37	R. E Kurshan and K. L. McMillan. Analysis of Digital Circuits Through Symbolic Reduction. IEEE Trans. CAD 10, pages 1356-1371, (1991).
	38	David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
	39	Z. Monna , A. Pnueli, Specification and verification of concurrent programs by A∀automata, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-2, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41626]
	40	Z. Manna and A. Pnueli. Tools and Rules for the Practicing Verifier. In Carnegie Mellon Computer Science: A 25-year Commemorative. ACM Press, 1990.
	41	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	42	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	43	Int'l. Conf. on Computer-Aided Verification. The proceedings to date have been published in Springer- Verlag's Lect. Notes in Comput. Sci. 407 (1989), 531 (1990), 575 (1991), 663 (1992), 697 (1993).
	44	James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
	45	Helmut Plünnecke , Wolfgang Reisig, Bibliography on Petri nets 1990, Papers from the 11th International Conference on Applications and Theory of Petri Net: Advances in Petri Nets 1991, p.317-572, June 01, 1990
	46	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	47	E J. Ramadge. Supervisory Control Problems for Discrete Event Systems Modeled by Btichi Automata. IEEE Transactions on Automatic Control 34, pages 10- 19, (1989).
	48	W. Savitch. Relationships Between Nondeterministic and Deterministic Tape Complexities. J. Computer Syst. Sci. 4, pages 177-192, (1970).
	49	Colin Stirling , David Walker, Local model checking in the modal mu-calculus, Theoretical Computer Science, v.89 n.1, p.161-177, Oct. 21, 1991
	50	M. Y. Vardi. Verification of Concurrent Programs The Automata-Theoretic Framework. In Proc. 2nd IEEE Syrup. on Logic in Computer Science, pages 161- 176, Ithaca, 1987.
	51	Moshe Y. Vardi, Unified Verification Theory, Temporal Logic in Specification, p.202-212, April 08-10, 1987
	52	Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
	53	M. Y. Vardi and E Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In Proc. IEEE Symp. on Logic in Computer Science, pages 332- 334, Boston, 1987.
	54	Bart Vergauwen , Johan Lewi, A Linear Local Model Checking Algorithm for CTL, Proceedings of the 4th International Conference on Concurrency Theory, p.447-461, August 23-26, 1993
	55	D. Walker. Bisimulations and Divergence in CCS. In Third Annual Symposium on Logic in Computer Science, pages 186-192. Computer Society Press, 1988.
	56	R Wolper. Temporal Logic Can Be More Expressive. Inf. Control 56, pages 72-99, (1983).
	57	Pierre Wolper, On the Relation of Programs and Computations to Models of Temporal Logic, Temporal Logic in Specification, p.75-123, April 08-10, 1987
	58	Pierre Wolper , Denis Leroy, Reliable Hashing without Collosion Detection, Proceedings of the 5th International Conference on Computer Aided Verification, p.59-70, June 28-July 01, 1993
	59	E L. Wolper, M. Y. Vardi, and A. E Sistla. Reasoning About Infinite Computation Paths. In Proc. 24th IEEE Symp. on Foundation of Computer Science, pages 185- 194, Tuscon, 1983. (To appear in Inf. Comput.).

CITED BY 3

	Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996
	Orna Kupferman , Moshe Y. Vardi, From complementation to certification, Theoretical Computer Science, v.345 n.1, p.83-100, 21 November 2005
	Jeff Edmonds , Chung-Keung Poon, A nearly optimal time-space lower bound for directed st-connectivity on the NNJAG model, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.147-156, May 29-June 01, 1995, Las Vegas, Nevada, United States