Formal methods

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 , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]
	2	D. P. Appenzeller, Formal verification of a PowerPC microprocessor, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.79, October 02-04, 1995
	3	ARCHINOFF, G. ET AL. 1990. Verification of the shutdown system software at the Darlington Nuclear Generating System. In International Conference on Control and Instrumentation in Nuclear Installations (Glasgow, Scotland, May).
	4	André Arnold , Didier Bégay , Jean-Pierre Radoux, The embedded software of an electricity meter: an experience in using formal methods in an industrial project, Science of Computer Programming, v.28 n.2-3, p.93-110, April 1997 [doi>10.1016/S0167-6423(96)00018-4]
	5	Geoff Barrett, Formal Methods Applied to a Floating-Point Number System, IEEE Transactions on Software Engineering, v.15 n.5, p.611-621, May 1989 [doi>10.1109/32.24710]
	6	Geoff Barrett, Model Checking in Practice: The T9000 Virtual Channel Processor, IEEE Transactions on Software Engineering, v.21 n.2, p.69-78, February 1995 [doi>10.1109/32.345823]
	7	Stephen Bear, An Overview of HP-SL, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.571-587, October 21-25, 1991
	8	Johan Bengtsson , W. O. David Griffioen , Kåre J. Kristoffersen , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi, Verification of an Audio Protocol with Bus Collision Using UPPAAL, Proceedings of the 8th International Conference on Computer Aided Verification, p.244-256, August 03, 1996
	9	Nikolaj Bjørner , Anca Browne , Eddie Chang , Michael Colón , Arjun Kapur , Zohar Manna , Henny Sipma , Tomás E. Uribe, STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems, Proceedings of the 8th International Conference on Computer Aided Verification, p.415-418, August 03, 1996
	10	Doeko Bosscher , Indra Polak , Frits W. Vaandrager, Verification of an Audio Control Protocol, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.170-192, September 19-23, 1994
	11	Anthony Boswell, Specification and Validation of a Security Policy Model, IEEE Transactions on Software Engineering, v.21 n.2, p.63-68, February 1995 [doi>10.1109/32.345822]
	12	Robert S. Boyer , Yuan Yu, Automated proofs of object code for a widely used microprocessor, Journal of the ACM (JACM), v.43 n.1, p.166-192, Jan. 1996 [doi>10.1145/227595.227603]
	13	BOYER, R. S. AND MooRE, J.S. 1979. A Computational Logic. Academic Press, New York.
	14	Robert S. Boyer , J. Strother Moore, A computational logic handbook, Academic Press Professional, Inc., San Diego, CA, 1988
	15	Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
	16	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
	17	M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
	18	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]
	19	BURCH, J. R., CLARKE, E. M., LONG, D. E., McMIL- LAN, K. L., AND DILL, D.L. 1994. Symbolic model checking for sequential circuit verification. IEEE Trans. Cornput. Aided Des. Integr. Circuits Syst. 13, 4 (April), 401-424.
	20	CALERO, J., ROMAN, C., AND PALMA, G.D. 1997. A practical design case using formal verification. In Proceedings of Design-SuperCon'97. To appear.
	21	CARNOT, M., DASILVA, C., DEHBONEI, B., AND MEIJA, F. 1992. Error-free software development for critical systems using the B-methodology. In Third International IEEE Symposium on Software Reliability Engineering.
	22	K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
	23	John A. Chaves, Formal Methods at AT&T - An Industrial Usage Report, Proceedings of the IFIP TC6/WG6.1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, IV, p.83-90, November 19-22, 1991
	24	Ghassan Chehaibar , Hubert Garavel , Laurent Mounier , Nadia Tawbi , Ferruccio Zulian, Specification and verification of the PowerScale bus arbitration protocol: an industrial experiment with LOTOS, IFIP TC6/ 6.1 international conference on formal description techniques IX/protocol specification, testing and verification XVI on Formal description techniques IX : theory, application and tools: theory, application and tools, p.435-450, January 1996, Kaiserslautern, Germany
	25	CHISOLM, G., KLJAICH, J., SMITH, B., AND WOJCIK, A. 1987. An approach to the verification of a fault -tolerant, computer-based reactor safety system: A case study using automated reasoning (Vol. 1, interim report). Tech. Rep. NP-4924 (Jan.), Electric Power Research Institute, Palo Alto, CA. Prepared by Argonne National Laboratory.
	26	Edmund M. Clarke , Steven M. German , Xudong Zhao, Verifying the SRT Division Algorithm Using Theorem Proving Techniques, Proceedings of the 8th International Conference on Computer Aided Verification, p.111-122, August 03, 1996
	27	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]
	28	CLARKE, E. AND ZHAO, X. 1993. Analytica: A theorem prover for Mathematica. Mathematica J., 56-71.
	29	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
	30	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]
	31	Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
	32	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]
	33	Rance Cleaveland , Eric Madelaine , Steve Sims, A Front-End Generator for Verification Tools, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.153-173, May 19-20, 1995
	34	Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
	35	R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	36	CORNES, C., COURANT, J., FILLIATRE, J.-C., HUET, G., MANOURY, P., PAULIN-MoHRING, C., MUNOZ, C., MURTttY, C., PARENT, C., SAYBI, A., AND WERNER, B. 1995. The coq proof assistant reference manual version 5.10. Tech. Rep. 177 (July), INRIA. http://pauillac.inria.fr/coq/systeme_coq-eng.html.
	37	CRAIGEN, D., GERttART, S., AND RALSTON, T. 1993a. An international survey of industrial applications of formal methods. Tech. Rep. NIST GCR 93/626 (Vols. 1 and 2) (March), U.S. National Institute of Standards and Technology. Also published by the U.S. Naval Research Laboratory (Formal Rep. 5546-93- 9582, Sept.), and the Atomic Energy Control Board of Canada.
	38	Susan Gerhart , Dan Craigen , Ted Ralston, Observations on industrial practice using formal methods, Proceedings of the 15th international conference on Software Engineering, p.24-33, May 17-21, 1993, Baltimore, Maryland, United States
	39	Susan Gerhart , Dan Craigen , Ted Ralston, Experience with Formal Methods in Critical Systems, IEEE Software, v.11 n.1, p.21-28, January 1994 [doi>10.1109/52.251198]
	40	Dan Craigen , Susan Gerhart , Ted Ralston, Formal Methods Reality Check: Industrial Usage, IEEE Transactions on Software Engineering, v.21 n.2, p.90-98, February 1995 [doi>10.1109/32.345825]
	41	D. Craigen , S. Kromodimoeljo , I. Meisels , A. Neilson , B. Pase , M. Saaltink, m-EVES: A tool for verifying software, Proceedings of the 10th international conference on Software engineering, p.324-333, April 11-15, 1988, Singapore
	42	Martin Croxford , James Sutton, Breaking Through the V and V Bottleneck, Proceedings of the Second International Eurospace - Ada-Europe Symposium on Ada in Europe, p.344-354, October 02-06, 1995
	43	W. Damm , Carlos Delgado Kloos, Practical Formal Methods for Hardware Design, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
	44	Werner Damm , Bernhard Josko , Rainer Schlör, Specification and verification of VHDL-based system-level hardware designs, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
	45	C. Daws , S. Yovine, Two examples of verification of multirate timed automata with Kronos, Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS '95), p.66, December 05-07, 1995
	46	David Déharbe , Dominique Borrione, Semantics of a verification-oriented subset of VHDL, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.293-310, October 02-04, 1995
	47	Norman Delisle , David Garlan, A Formal Specification of an Oscilloscope, IEEE Software, v.7 n.5, p.29-36, September 1990 [doi>10.1109/52.57890]
	48	DEPALMA, G. AND GLASER, A. 1996. Formal verification augments simulation. Electr. Eng. Times, 56.
	49	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	50	DINOLT, G. ET AL. 1984. Multinet gateway--towards A1 certification. In IEEE Symposium on Security and Privacy (1984).
	51	Wael M. Elseaidy , Rance Cleaveland , John W. Baugh, Jr., Modeling and verifying active structural control systems, Science of Computer Programming, v.29 n.1-2, p.99-122, July 1997 [doi>10.1016/S0167-6423(96)00031-7]
	52	F~RNAND~Z, J.-C., GARAVEL, H., KEaBRAT, A., MA- TEESCU, e., MOUNIER, L., AND SIGHIREANU, M. 1996. CADP (CfESAR/ALDEBARAN development package): A protocol validation and international verification toolbox. In Proceedings of the 8th Conference on Computer- Aided Verification, Number 1102 in Lecture Notes in Computer Science. R. Alur and T. A. Henzinger, Eds., Springer-Verlag.
	53	FILKORN, T., SCH~mIDER, H., SCHOLZ, A., STRASSER, A., AND WARKENTIN, P. 1994. SVE User's Guide. Tech. Rep. ZFE BT SE 1-SVE-1, Siemens AG, Corporate Research and Development, Munich.
	54	David Garlan , Alan W. Brown , Daniel Jackson , James E. Tomayko , Jeannette M. Wing, The CMU Master of Software Engineering Core Curriculum, Proceedings of the 8th SEI CSEE Conference on Software Engineering Education, p.65-86, March 29-April 01, 1995
	55	S.J. Garland , J. V. Guttag, Inductive methods for reasoning about abstract data types, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.219-228, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73579]
	56	Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
	57	GORDON, M. 1987. HOL: A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis. Kluwer.
	58	GORDON, M. J., MILNER, A. J., AND WADSWORTH, C. P. 1979. Edinburgh LCF, Vol. 78 of Lecture Notes in Computer Science. Springer- Verlag.
	59	G. Guiho , C. Hennebert, SACEM software validation, Proceedings of the 12th international conference on Software engineering, p.186-191, March 26-30, 1990, Nice, France
	60	John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
	61	Anthony Hall, Using Formal Methods to Develop an ATC Information System, IEEE Software, v.13 n.2, p.66-76, March 1996 [doi>10.1109/52.506463]
	62	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	63	David Harel, Biting the Silver Bullet: Toward a Brighter Future for System Development, Computer, v.25 n.1, p.8-20, January 1992 [doi>10.1109/2.161283]
	64	HAR'EL, Z. AND KURSHAN, R.P. 1990. Software for analytical development of communications protocols. AT&T Bell Lab. Tech. J. 69, I (Jan.- Feb.), 45-59.
	65	Mats P. E. Heimdahl , Nancy G. Leveson, Completeness and Consistency in Hierarchical State-Based Requirements, IEEE Transactions on Software Engineering, v.22 n.6, p.363-377, June 1996 [doi>10.1109/32.508311]
	66	HENINGER, K. 1980. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. Softw. Eng. 6, I (Jan.), 2-13.
	67	Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
	68	Pei-Hsin Ho , Howard Wong-Toi, Automated Analysis of an Audio Control Protocol, Proceedings of the 7th International Conference on Computer Aided Verification, p.381-394, July 03-05, 1995
	69	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	70	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
	71	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	72	Gerard J. Holzmann, Practical methods for the formal validation of SDL specifications, Computer Communications, v.15 n.2, p.129-134, March 1992 [doi>10.1016/0140-3664(92)90132-X]
	73	HOLZMANN, G. 1994. The theory and practice of a formal method: NewCoRe. In Proceedings of IFIP World Computer Congress (Hamburg, Germany, Aug.).
	74	Gerard J. Holzmann , Joanna Patti, Validating SDL Specifications: an Experiment, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.317-326, June 06-09, 1989
	75	Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
	76	Ian Houston , Steve King, CICS Project Report: Experiences and Results from the use of Z in IBM, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.588-596, October 21-25, 1991
	77	ISO. 1987. Information Systems Processing-- Open Systems Interconnection--LOTOS. Tech. Rep. International Standards Organization DIS 8807.
	78	Jonathan Jacky, Specifying a Safety-Critical Control System in Z, IEEE Transactions on Software Engineering, v.21 n.2, p.99-106, February 1995 [doi>10.1109/32.345826]
	79	Lalita Jategaonkar Jagadeesan , Carlos Puchol , James E. Von Olnhausen, A formal approach to reactive systems software: a telecommunications application in ESTEREL, Formal Methods in System Design, v.8 n.2, p.123-151, March 1996 [doi>10.1007/BF00122418]
	80	Ryszard Janicki , David Lorge Parnas , Jeffery Zucker, Tabular representations in relational documents, Relational methods in computer science, Springer-Verlag New York, Inc., New York, NY, 1997
	81	C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
	82	Markus Kaltenbach, Model Checking for UNITY, University of Texas at Austin, Austin, TX, 1994
	83	Deepak Kapur , David R. Musser, Proof by consistency, Artificial Intelligence, v.31 n.2, p.125-157, Feb. 1987 [doi>10.1016/0004-3702(87)90017-8]
	84	KAUFMANN, M. AND MOORE, J.S. 1995. ACL2: A Computational Logic for Applicative Common Lisp, The User's Manual (Version 1.8). ftp:// ftp.cli.com/pub/acl2/v1-8/acl2-sources/doc/ HTM L/acl2-doc.html.
	85	KINDRED, D. AND WING, J. 1996. Fast, automatic checking of security protocols. In Proceedings of the USENIX Workshop on Electronic Commerce Protocols (1996).
	86	Trevor King, Formalising British Rail's Signalling Rules, Proceedings of the Second International Symposium of Formal Methods Europe on Industrial Benefit of Formal Methods, p.45-54, October 24-18, 1994
	87	J. Kljaich, Jr. , B. T. Smith , A. S. Wojcik, Formal Verification of Fault Tolerance Using Theorem-Proving Techniques, IEEE Transactions on Computers, v.38 n.3, p.366-376, March 1989 [doi>10.1109/12.21123]
	88	A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
	89	KUHN, D. AND DRAY, J. 1990. Formal specification and verification of control software for cryptographic equipment. In Sixth Computer Security Applications Conference (1990).
	90	Robert P. Kurshan , Leslie Lamport, Verification of a Multiplier: 64 Bits and Beyond, Proceedings of the 5th International Conference on Computer Aided Verification, p.166-179, June 28-July 01, 1993
	91	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	92	R. P. Kurshan, The complexity of verification, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.365-371, May 23-25, 1994, Montreal, Quebec, Canada [doi>10.1145/195058.195194]
	93	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
	94	Pierre Lescanne, Computer experiments with the REVE term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.99-108, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567078]
	95	David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
	96	Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
	97	Luo, Z. AND POLLACK, R. 1992. LEGO proof development system: User's manual. Tech. Rep. ECS-LFCS-92-211 (May), Computer Science Dept., Univ. of Edinburgh.
	98	N. A. Lynch , M. Tuttle, HIERARCHICAL CORRECTNESS PROOFS FOR DISTRIBUTED ALGORITHMS, Massachusetts Institute of Technology, Cambridge, MA, 1987
	99	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	100	MATAGA, P. AND ZAVE, P. 1995. Multiparadigm specification of an AT&T switching system. In Applications of Formal Methods, M. G. Hinchey and J. P. Bowen, Eds., Prentice-Hall International, Englewood Cliffs, NJ, 375-398.
	101	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	102	S. P. Miller , M. Srivas, Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.2, April 05-08, 1995
	103	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	104	MOORE, J. S., LYNCH, T., AND KAUFMANN, M. 1996. A mechanically checked proof of the correctness of the AMD5K86 floating point division algorithm, http://devil.ece.utexas.edu :80/lynch/ divide/divide.html.
	105	Mogens Nielsen , Klaus Havelund , Kim Ritter Wagner , Chris George, The RAISE language, methods and tools, Formal Aspects of Computing, v.1 n.1, p.85-114, Jan.-March 1989 [doi>10.1007/BF01887199]
	106	Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
	107	OXFORD UNIVERSITY. 1996. http://www.oomlab. ox.ac.uk/igdp/. Master's of Science in Software Engineering.
	108	Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
	109	PNUELI, A. 1981. A temporal logic of concurrent programs. Theor. Comput. Sci. 13, 45-60.
	110	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
	111	S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995
	112	D. Richardson , O. O'Malley , C. Tittle, Approaches to specification-based testing, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.86-96, December 13-15, 1989, Key West, Florida, United States
	113	A. W. Roscoe, Model-checking CSP, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
	114	Valérie Roy , Robert de Simone, Auto/Autograph, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.65-75, June 18-21, 1990
	115	Harald Rueß , Natarajan Shankar , Mandayam K. Srivas, Modular Verification of SRT Division, Proceedings of the 8th International Conference on Computer Aided Verification, p.123-134, August 03, 1996
	116	RUSSINOFF, D. 1996. A mechanically checked proof of the correctness of the AMD K5 floating-point square root algorithm (submitted).
	117	SPC. 1993. Consortium requirements engineering guidebook. Tech. Rep. SPC-92060-CMC version 01.00.09, Software Productivity Consortium, Herndon, VA.
	118	J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
	119	STEFFEN, B., MARGARIA, T., CLASSEN, A., AND BRAUN, V. 1996. The Meta '95 environment. In Proceedings of Computer-Aided Verification '96, Lecture Notes Computer Science, Springer-Verlag.
	120	STEFFEN, B., MARGARIA, T., CLASSEN, A., BRAUN, V., AND REITENSPIESS, M. 1996. An environment for the creation of intelligent network services. In Intelligent Networks: IN/AIN Technologies, Operations, Services, and Applications--A Comprehensive Report (Chicago), I. E. Consortium Ed., 287-300. Invited contribution. Also invited to the Annual Review of Communications, IEC, 919-935.
	121	VARDI, M. Y. AND WOLPER, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of Logic in Computer Science.
	122	WING, J. 1985. Specification firms: A vision for the future. In Proceedings of the Third International Workshop on Software Specification and Design (London, Aug.), 241-243.
	123	Pamela Zave, Secrets of Call Forwarding: A Specification Case Study, Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques VIII, p.169-184, October 01, 1995
	124	Pamela Zave , Michael Jackson, Where Do Operations Come From? A Multiparadigm Specification Technique, IEEE Transactions on Software Engineering, v.22 n.7, p.508-528, July 1996 [doi>10.1109/32.538607]