Edmund M. Clarke
Jeannette M. Wing
- ALUR, R., HENZINGER, T., AND HO, P.-H. 1996. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22, 3, 181- 201. Google Scholar
Digital Library
- APPENZELLER, U. P. AND KUEHLMANN, A. 1995. Formal verification of a PowerPC microprocessor. In Proceedings of the IEEE International Conference on Computer Design (ICCD'95) (Austin, TX, Oct.), 79-84. Google Scholar
- 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).Google Scholar
- ARNOLD, A., BEGAY, D., AND RADOUX, J.-P. 1996. The embedded software of an electricity meter: An experience in using Formal Methods in an industrial project. Sci. Cornput. Program. Google Scholar
- BARRETT, G. 1989. Formal methods applied to a floating-point number system. IEEE Trans. Softw. Eng. 15, 5 (May), 611-621. Google ScholarDigital Library
- BARRETT, G. 1995. Model checking in practice: The t9000 virtual channel processor. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 69-78. Google ScholarDigital Library
- BEAR, S. 1991. An overview of HP-SL. In Proceedings of VDM'91: Formal Development Methods, Volume 551 of Lecture Notes in Computer Science. Springer-Verlag. Google Scholar
- BENGTSSON, J., GRIFFIOEN, W., KRISTOFFERSEN, K., LARSEN, K., LARSSON, F., PETTERSSON, P., AND YI, W. 1996. Verification of an audio protocol with bus collision using UppAal. In Cornputer-Aided Verification '96, Lecture Notes in Computer Science 1102, R. Alur and T. Henzinger, Eds., Springer-Verlag, 244-256. Google Scholar
- BJORNER, N. ET AL. 1996. STEP: Deductive-algorithmic verification of reactive and real-time systems. In Proceedings of the Eighth International Conference on Computer-Aided Verification, Number 1102 in Lecture Notes in Computer Science (July), Springer-Verlag, 415-418. Google Scholar
- Bossc~zR, D., POLAK, I., Ai,~ VAANDRAGER, F. 1994. Verification of an audio-control protocol. In FTRTFT 94: Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, H. Langmaack, W.-P. de Roever, and J. Vytopil Eds., Springer-Verlag, 170-192. Google Scholar
- BOSWELL, A. 1995. Specification and validation of a security policy model. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 63-68. Google ScholarDigital Library
- BOYER, R. AND Yu, Y. 1996. Automated proofs of object code for a widely used microprocessor. J. ACM 43, 1 (Jan.), 166-192. Google ScholarDigital Library
- BOYER, R. S. AND MooRE, J.S. 1979. A Computational Logic. Academic Press, New York.Google Scholar
- BOYER, R. S. AND MooRE, J.S. 1988. A Computational Logic Handbook. Academic Press, New York. Google Scholar
- BRAYTON, R. ET AL. 1996. VIS: A system for verification and synthesis. In Proceedings of the Eighth International Conference on Cornputer-Aided Verification, Number 1102 in Lecture Notes in Computer Science, Springer- Verlag, 423-427. Google Scholar
- BROCK, B., KAUFMANN, M., AND MOORE, J. S. 1996. Heavy inference: Theorems about commercial microprocessors. In Formal Methods in Computer-Aided Design (FMCAD'96) (Nov.), M. Srivas and A. Camilleri Eds., Springer-Verlag. Google Scholar
- BROWNE, M. C., CLARKE, E. M., DILL, D. L., AND MISHRA, B. 1986. Automatic verification of sequential circuits using temporal logic. IEEE Trans. Comput. C-35, 12, 1035-1044. Google ScholarDigital Library
- BRYANT, R. E. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Cornput. C-35, 8. Google Scholar
- 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.Google ScholarDigital Library
- CALERO, J., ROMAN, C., AND PALMA, G.D. 1997. A practical design case using formal verification. In Proceedings of Design-SuperCon'97. To appear.Google Scholar
- 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.Google Scholar
- CHANDY, K. AND MISRA, J. 1988. Parallel Program Design. Addison-Wesley, Reading, MA. Google Scholar
- CHAVES, J. 1992. Formal methods at AT&T: An industrial usage report. In Proceedings Forreal Description Techniques IV - 1991, North- Holland, Amsterdam, 83-90. Google Scholar
- CHEHAIBAR, G., GARAVEL, H., MOUNIER, L., TAWBI, N., AND ZULIAN, F. 1996. Specification and verification of the powerscale bus arbitration protocol: An industrial experiment with LO- TOS. In Proceedings of FORTE/PSTV'96 (Kaiserslautern, Germany). Chapman & Hall, London. Google Scholar
- 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.Google Scholar
- CLARKE, E., GERMAN, S., AND ZHAO, X. 1996. Verifying the SRT division algorithm using theorem proving techniques. In Proceedings of the Eighth International Conference on Computer-Aided Verification, Number 1102 in Lecture Notes in Computer Science, Springer- Verlag, 111-122. Google Scholar
- CLARKE, E. AND KURSHAN, R. 1996. Computeraided verification. IEEE Spectrum 33, 6, 61- 67. Google ScholarDigital Library
- CLARKE, E. AND ZHAO, X. 1993. Analytica: A theorem prover for Mathematica. Mathematica J., 56-71.Google Scholar
- CLARKE, E. M. AND EMERSON, E.A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, (Yorktown Heights, NY), Vol. 131 of Lecture Notes in Computer Science, Springer-Verlag. Google Scholar
- CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Trans. Program Lang. Syst. 8, 2, 244-263. Google ScholarDigital Library
- CLARKE, E. M., GRUMBERG, O., HIRAISHI, H., JHA, S., LONG, D. E., McMILLAN, K. L., AND NESS, L. A. 1993. Verification of the Futurebus+ cache coherence protocol. In Proceedings CHDL. Google Scholar
- CLARKE, E. M., GRUMBERG, O., AND LONG, D. E. 1992. Model checking and abstraction. In Proceedings of Principles of Programming Languages. Google Scholar
- CLEAVELAND, R., MADELAINE, E., AND SIMS, S. 1995. Generating front ends for verification tools. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), Vol. 1019 of Lecture Notes in Computer Science, E. Brinksma, R. Cleaveland, K. Larsen, and B. Steffen Eds., Springer-Verlag, 153-173. Google Scholar
- CLEAVELAND, R., PARROW, J., AND STEFFEN, B. 1993. The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Trans. Program Lang. Syst. 15, 1 (Jan.), 36-72. Google ScholarDigital Library
- CONSTABLE, R. ET AL. 1986. Implementing Mathematics with the NuPRL Proof Develop- ,tent Environment. Prentice-Hall, Englewood Cliffs, NJ. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- CRAIGEN, D., GERHART, S., AND RALSTON, T. 1993b. Observations on industrial practice using formal methods. In Proceedings of the Fifteenth International Conference on Software Engineering (May). Google Scholar
- CRAIGEN, D., GERHART, S., AND RALSTON, T. 1994. Formal methods in critical systems. IEEE Softw. 11, 1 (Jan.). Google Scholar
- CRAIGEN, D., GERHART, S., AND RALSTON, T. 1995. Formal methods reality check: Industrial usage. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 90 -98. Google ScholarDigital Library
- CRAIGEN, D., KROMODIMOELJO, S., MEISELS, I., NEILSON, A., PASE, B., AND SAALTINK, M. 1988. m-EVES: A tool for verifying software. In Proceedings of the Tenth International Conference on Software Engineering (Singapore, April), 324-333. Google Scholar
- CROXFORD, M. AND SUTTON, J. 1995. Breaking through the V and V bottleneck. In Proceedings of Ada in Europe 1995. Springer-Verlag. Google Scholar
- DAMM, W. AND DELGADO-KLoos, C. 1996. Practical Formal Methods for Hardware Design. Lecture Notes in Computer Science. Springer-Verlag. Google Scholar
- DAMM, W., JOSKO, B., AND SCHLOR, R. 1995. Specification and Validation Methods for Programming Languages and Systems, Chap. Specification and verification of VHDL-based system-level hardware designs, Oxford University Press, New York, 331-410. Google Scholar
- DAWS, C. AND YOVINE, S. 1995. Two examples of verification of multirate timed automata with KRONOS. In Proceedings of 1995 IEEE Real- Time Systems Symposium, RTSS'95 (Pisa, Italy, Dec.). IEEE Computer Society Press, Los Alamitos, CA. Google Scholar
- DEHARBE, D. AND BORRIONE, D. 1995. Semantics of a verification-oriented subset of VHDL. In CHARME'95, Correct Hardware Design and Verification Methods, P. Camurati and H. Eveking, Eds., Vol. 987 of Lecture Notes in Computer Science Springer-Verlag, 293-310. Google Scholar
- DELISLE, N. AND GARLAN, D. 1990. A formal specification of an oscilloscope. IEEE Softw. 7, 5 (Sept.), 29-36. Google Scholar
- DEPALMA, G. AND GLASER, A. 1996. Formal verification augments simulation. Electr. Eng. Times, 56.Google Scholar
- DILL, D. L., DaEXL~R, A. J., Hu, A. J., A~D YANG, C. H. 1992. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, 522-525. Google Scholar
- DINOLT, G. ET AL. 1984. Multinet gateway--towards A1 certification. In IEEE Symposium on Security and Privacy (1984).Google Scholar
- ELSEAIDY, W., CLEAVELAND, R., AND BAUGH, J. 1996. Modeling and verifying active structural control systems. Sci. Comput. Program. (to appear). A preliminary version of this paper appears in the Proceedings of the 1994 Real-Time Systems Symposium. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- GARLAN, D., ABOWD, G., JACKSON, D., TOMAYKO, J., AND WING, J. 1995. The CMU Master of Software Engineering Core Curriculum. In Proceedings of the Eighth SEI Conference on Software Engineering Education (CSEE) Vol. 895 of Lecture Notes in Computer Science, Springer-Verlag, 65-86. Google Scholar
- GARLAND, S. J. AND GUTTAG, J. V. 1988. Inductive methods for reasoning about abstract data types. In Proceedings of the Fifteenth Symposium on Principles of Programruing Languages, 219-228. Google Scholar
- GERTH, R., PEL~D, D., VARDI, M. Y., A~D WOLP~R, P. 1995. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings IFIP/WG6.1 Symposium on Protocol Specification, Testing, and Verification (Warsaw, Poland, June). Google Scholar
- GORDON, M. 1987. HOL: A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis. Kluwer.Google Scholar
- GORDON, M. J., MILNER, A. J., AND WADSWORTH, C. P. 1979. Edinburgh LCF, Vol. 78 of Lecture Notes in Computer Science. Springer- Verlag.Google Scholar
- GUIHO, G. AND HENNEBERT, C. 1990. SACEM software validation. In Twelfth International Conference on Software Engineering. Google Scholar
- GUTTAG, J. AND HORNING, J. 1993. Larch: Languages and Tools for Formal Specification. Springer-Verlag. Written with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Google ScholarDigital Library
- HALL, A. 1996. Using formal methods to develop an ATC information system. IEEE Softw. 12, 6 (March), 66-76. Google Scholar
- HAREL, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Cornput. Program. 8, 231-274. Preliminary version: Tech. Rep. CS84-05, The Weizmann Institute of Science, Rehovot, Israel, Feb. 1984. Google ScholarDigital Library
- HAREL, D. 1992. Biting the silver bullet: Toward a brighter future for system development. IEEE Cornput. 25, I (Jan.), 8-20. Google ScholarCross Ref
- 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.Google ScholarCross Ref
- HEIMDAHL, M. AND LEVESON, N. 1996. Completeness and consistency in hierarchical statebased requirements. IEEE Trans. Softw. Eng. SE-22, 6 (June), 363-377. Google ScholarDigital Library
- HENINGER, K. 1980. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. Softw. Eng. 6, I (Jan.), 2-13.Google ScholarDigital Library
- H~NZIN6~R, T. A., NICOLLIN, X., SIFAKIS, J., AND YOVINE, S. 1994. Symbolic model checking for real-time systems. Inf. Comput. 111, 111- 244. Google Scholar
- Ho, P.-H. AND WONG-ToI, H. 1995. Automated analysis of an audio control protocol. In Computer-Aided Verification '95, Lecture Notes in Computer Science 939, P. Wolper Ed., Springer-Verlag, 381-394. Google Scholar
- HOARE, C. A.R. 1985. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ. Google Scholar
- HOJATI, R., BRAYTON, R., AND KURSHAN, R. 1993. BDD-based debugging of designs using language containment and fair CTL. In Proceedings of the Fifth International Conference on Computer-Aided Verification, Number 697 in Lecture Notes in Computer Science, C. Courcoubetis Ed., Springer-Verlag, 41-57. Google Scholar
- HOLZMANN, G. 1991. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey. Google Scholar
- HOLZMANN, G. 1992. Practical methods for the formal validation of SDL specifications. Cornput. Commun. Special issue on Practical Uses of FDT's. Google Scholar
- HOLZMANN, G. 1994. The theory and practice of a formal method: NewCoRe. In Proceedings of IFIP World Computer Congress (Hamburg, Germany, Aug.).Google Scholar
- HOLZMANN, G. AND PATTI, J. 1989. Validating SDL specifications: An experiment. In Proceedings of the Ninth International Conference on Protocol Specification, Testing, and Verification, INWG/IFIP (Twente, Netherlands, June) C. Vissers and E. Brinksma, Eds. Google Scholar
- HOLZMANN, G. AND PELED, D. 1994. An improvement in formal verification. In Proceedings of FORTE94 (Berne, Switzerland, Oct.). Google Scholar
- HOUSTON, I. AND KING, S. 1991. CICS project report: Experiences and results from using Z. In Proceedings of VDM'91: Formal Development Methods, Volume 551 of Lecture Notes in Computer Science, Springer-Verlag. Google Scholar
- ISO. 1987. Information Systems Processing-- Open Systems Interconnection--LOTOS. Tech. Rep. International Standards Organization DIS 8807.Google Scholar
- JACKY, J. 1995. Specifying a safety-critical control system in Z. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 99-106. Google ScholarDigital Library
- JAGADEESAN, L., PUCHOL, C., AND OLNHAUSEN, J. V. 1996. A formal approach to reactive systems software: A telecommunications application in Esterel. Formal Aspects Comput. 8, 2 (March), 123-151. Google Scholar
- JANICKI, R., PARNAS, D. L., AND ZUCKER, J. 1996. Tabular representations in relational documents. In Relational Methods in Computer Science. C. Brink, Ed., Springer-Verlag (to appear). Google Scholar
- JONES, C.B. 1986. Systematic Software Development Using VDM. Prentice-Hall International, New York. Google Scholar
- KALTENBACH, M. 1994. Model checking for UNITY. Tech. Rep. TR94-31 (Dec.), The University of Texas at Austin. Google Scholar
- KAPUR, D. AND MUSSER, D. 1987. Proof by consistency. Artif. Intell. 31, 125-157. Google ScholarDigital Library
- 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.Google Scholar
- KINDRED, D. AND WING, J. 1996. Fast, automatic checking of security protocols. In Proceedings of the USENIX Workshop on Electronic Commerce Protocols (1996). Google Scholar
- KING, T. 1994. Formalising British Rail's signalling rules. In FME'94: Industrial Benefit of Formal Methods, Volume 873 of Lecture Notes in Computer Science (1994), Springer- Verlag, 45-54. Google Scholar
- KLJAICH, J., SMITH, B., AND WOJCIK, A. 1989. Formal verification of fault tolerance using theorem-proving techniques. IEEE Trans. Comput. 38, 366-376. Google ScholarDigital Library
- KU~HLMANN, A., SRINIVASAN, A., AND LAPOTIN, D. P. 1995. Verity--a formal verification program for custom CMOS circuits. IBM J. Res. Dev. 39, 1/2, 149-165. Google Scholar
- KUHN, D. AND DRAY, J. 1990. Formal specification and verification of control software for cryptographic equipment. In Sixth Computer Security Applications Conference (1990).Google ScholarCross Ref
- KURSHAN, R. AND LAMPORT, L. 1993. Verification of a multiplier: 64 Bits and beyond. In Computer Aided Verification, Volume 697 of Lecture Notes in Computer Science, C. Courcoubetis, Ed., Springer-Verlag, 166-179. Google Scholar
- KURSHAN, R. P. 1994a. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ. Google Scholar
- KURSHAN, R.P. 1994b. The complexity of verification. In Proceedings 26th ACM Symposium on Theolg, of Computing (STOC) (Montreal), 365-371. Google Scholar
- LAMPORT, L. 1984. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 872- 923. Google Scholar
- LESCANNE, P. 1983. Computer experiments with the REVE term rewriting system generator. In Proceedings of the Tenth Symposium on Principles of Programming Languages (Austin, Texas, Jan.), 99-108. Google Scholar
- LONG, D.L. 1993. Model checking, abstraction, and compositional reasoning. Ph.D. Thesis, Carnegie Mellon Univ., Computer Science Dept. Google Scholar
- LOWE, G. 1996. Breaking and fixing the Needham-Schroder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Vol. 1055 of Lecture Notes in Computer Science. Springer-Verlag. Google Scholar
- 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.Google Scholar
- LYNCH, N. AND TUTTLE, M. 1987. Hierarchical correctness proofs for distributed algorithms. Tech. Rep. (April), MIT Laboratory for Computer Science, Cambridge, MA. Google Scholar
- MANNA, Z. AND PNUELI, A. 1991. The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, New York. Google Scholar
- 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.Google Scholar
- McMILLAN, K.L. 1993. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer. Google Scholar
- MILLER, S. P. AND SRIVAS, M. 1995. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT'95: Workshop on Industrial-Strength Formal Specification Techniques (Boca Raton, FL), IEEE Computer Society, Washington, DC, 2-16. Google Scholar
- MILNER, A. 1980. A Calculus of Communicating Systems, Vol. 92 of Lecture Notes in Computer Science. Springer-Verlag. Google Scholar
- 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.Google Scholar
- NIELSEN, M., HAVELUND, K., WAGNER, K., AND GEORGE, C. 1989. The RAISE language, method and tools. Formal Aspects Comput. 1, 85-114. Google ScholarCross Ref
- OwRE, S., RUSHBY, J., AND SHANKAR, N. 1992. PVS: A prototype verification system. In Eleventh International Conference on Automated Deduction (CADE), Vol. 607 of Lecture Notes in Artificial Intelligence, D. Kapur Ed., Springer-Verlag, 748-752. Google Scholar
- OXFORD UNIVERSITY. 1996. http://www.oomlab. ox.ac.uk/igdp/. Master's of Science in Software Engineering.Google Scholar
- PELED, D. 1996. Combining partial order reductions with on-the-fly model-checking. J. Forreal Meth. Syst. Des. 8 (1), 39-64. Also appeared in the Proceedings of the Sixth International Conference on Computer Aided Verification 1994 (Stanford, CA), Lecture Notes in Computer Science 818, Springer-Verlag, 377-390. Google ScholarCross Ref
- PNUELI, A. 1981. A temporal logic of concurrent programs. Theor. Comput. Sci. 13, 45-60.Google ScholarCross Ref
- QUEILLE, J. AND SIFAKIS, J. 1982. Specification and verification of concurrent systems in CALSAR. In Proceedings of Fifth ISP. Google Scholar
- RAJAN, S., SttANKAR, N., AND SRIVAS, M. 1995. An integration of model-checking with automated proof checking. In Computer-Aided Verification, '95, Volume 939 of Lecture Notes in Computer Science P. Wolper, Ed., Springer-Verlag, 84-97. Google Scholar
- RICHARDSON, D., O'MALLEY, T., AND MOORE, C. T. 1989. Approaches to specification-based testing. In ACM SIGSOFT 89: Third Symposium on Software Testing, Analysis, and Verification (Dec.). Google Scholar
- RoscoE, A. 1994. Model-checking CSP. In A Classical Mind: Essays in Honour of C.A.R. Hoare, A. Roscoe, Ed., Prentice-Hall, Englewood Cliffs, NJ. Google Scholar
- RoY, V. AND DE SIMONE, R. 1990. Auto/Autograph. In Computer-Aided Verification '90, Vol. 3 of DIMACS Series on Discrete Mathematics and Theoretical Computer Science (Piscataway, NJ, June), E. Clarke and R. Kurshan, Eds., American Mathematical Society, Providence, RI, 235-250. Google Scholar
- Ruzss, H., S~ANKAR, N., AND SRIVAS, M. 1996. Modular verification of SRT division. In Proceedings of the Eighth International Conference on Computer-Aided Verification, No. 1102 in Lecture Notes in Computer Science (July), Springer-Verlag, 123-134. Google Scholar
- RUSSINOFF, D. 1996. A mechanically checked proof of the correctness of the AMD K5 floating-point square root algorithm (submitted).Google Scholar
- SPC. 1993. Consortium requirements engineering guidebook. Tech. Rep. SPC-92060-CMC version 01.00.09, Software Productivity Consortium, Herndon, VA.Google Scholar
- SPIVEY, J.n. 1988. Introducing Z: a Specification Language and its Formal Semantics. Cambridge University Press, New York. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- VARDI, M. Y. AND WOLPER, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of Logic in Computer Science.Google Scholar
- 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.Google Scholar
- ZAVE, P. 1995. Secrets of call forwarding: A specification case study. In Proceedings of the Eighth International IFIP Conference on Forreal Description Techniques for Distributed Systems and Communications Protocols (FORTE '95) Chapman & Hall, London, 153- 168. Google Scholar
- ZAVE, P. AND JACKSON, M. 1996. Where do operations come from? A multiparadigm specification technique. IEEE Trans. Softw. Eng. 22, 7 (July), 508-528. Google ScholarDigital Library
Index Terms
- Formal methods: state of the art and future directions
Recommendations
Survey on Formal Verification Methods for Digital IC
ICICSE '09: Proceedings of the 2009 Fourth International Conference on Internet Computing for Science and EngineeringThis paper presents a survey of the state-of-art of formal verification technique. The expression models for formal verification are introduced and analyzed. The characteristics of each model are expounded. Moreover, the typical model checking ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Improving simulation-based verification by means of formal methods
ASP-DAC '04: Proceedings of the 2004 Asia and South Pacific Design Automation ConferenceThe design of complex systems is largely ruled by the time needed for verification. Even though formal methods can provide higher reliability, in practice often simulation based verification is used. Large testbenches are created and if the design ...
Comments