{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T14:46:11Z","timestamp":1747579571940},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540559634"},{"type":"electronic","value":"9783540473305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55963-9_45","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:47:02Z","timestamp":1330253222000},"page":"131-142","source":"Crossref","is-referenced-by-count":5,"title":["Formal methods for software engineers: Tradeoffs in curriculum design"],"prefix":"10.1007","author":[{"given":"David","family":"Garlan","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,7,11]]},"reference":[{"issue":"12","key":"11_CR1","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/MC.1979.1658580","volume":"12","author":"T. Agerwala","year":"1979","unstructured":"T. Agerwala. Putting Petri nets to work. Computer, 12(12):85\u201394, December 1979.","journal-title":"Computer"},{"key":"11_CR2","volume-title":"ASLAN User's Manual","author":"B. Auernheimer","year":"1984","unstructured":"B. Auernheimer and R.A. Kemmerer. ASLAN User's Manual. Dept. of Computer Science, UC Santa Barbara, 1984."},{"issue":"5","key":"11_CR3","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"G. Barrett","year":"1989","unstructured":"G. Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15(5):611\u2013621, May 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"W.C. Bowman, G.H. Archinoff, V.M. Raina, D.R. Tremaine, and N.G. Leveson. An application of fault tree analysis to safety critical software at Ontario Hydro. In Conference on Probabilistic Safety Assessment and Management (PSAM), April 1991.","key":"11_CR4"},{"unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, June 1990.","key":"11_CR5"},{"unstructured":"Problem set for the fourth international workshop on software specification and design. ACM SIGSOFT Engineering Notes, April 1986, 1986.","key":"11_CR6"},{"unstructured":"B. Cohen, W.T. Harwood, and M.I. Jackson. The Specification of Complex Systems. Addison-Wesley, 1986. (Chapter 5: Model-based specification).","key":"11_CR7"},{"doi-asserted-by":"crossref","unstructured":"J.P. Cavano and J.A. McCall. A framework for the measurement of software quality. In Software Quality and Assurance Workshop, pages 133\u2013139. ACM, November 1978.","key":"11_CR8","DOI":"10.1145\/800283.811113"},{"issue":"5","key":"11_CR9","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/52.57890","volume":"7","author":"N. Delisle","year":"1990","unstructured":"N. Delisle and D. Garlan. A formal specification of an oscilloscope. Software, 7(5):29\u201337, September 1990.","journal-title":"Software"},{"key":"11_CR10","volume-title":"LNCS 428","author":"D. Garlan","year":"1990","unstructured":"David Garlan and Norman Delisle. Formal specifications as reusable frameworks. In VDM'90: VDM and Z \u2014 Formal Methods in Software Development, Kiel, Germany, 1990. Springer-Verlag, LNCS 428."},{"doi-asserted-by":"crossref","unstructured":"J.V. Guttag and J.J. Horning. Formal specification as a design tool. In Seventh POPL. ACM, 1980. (also in Software Specification Techniques, pages 187\u2013207).","key":"11_CR11","DOI":"10.1145\/567446.567471"},{"doi-asserted-by":"crossref","unstructured":"J.V. Guttag, E. Horowitz, and D.R. Musser. Abstract data types and software validation. Communications of the ACM, 21(12), December 1978.","key":"11_CR12","DOI":"10.1145\/359657.359666"},{"unstructured":"J.V. Guttag, J.J. Horning, and M. Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Digital, Systems Research Center, 1990.","key":"11_CR13"},{"issue":"5","key":"11_CR14","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/MS.1985.231756","volume":"2","author":"J.V. Guttag","year":"1985","unstructured":"J.V. Guttag, J.J. Horning, and J.M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24\u201336, September 1985.","journal-title":"IEEE Software"},{"doi-asserted-by":"crossref","unstructured":"David Garlan and David Notkin. Formalizing design spaces: Implicit invocation mechanisms. In VDM'91: Formal Software Development Methods, pages 31\u201344. Springer-Verlag, LNCS 551, October 1991.","key":"11_CR15","DOI":"10.1007\/3-540-54834-3_5"},{"doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer-Verlag, 1981.","key":"11_CR16","DOI":"10.1007\/978-1-4612-5983-1"},{"issue":"5","key":"11_CR17","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A. Hall","year":"1990","unstructured":"A. Hall. Seven myths of formal methods. Software, 7(5):11\u201320, September 1990.","journal-title":"Software"},{"key":"11_CR18","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"issue":"8","key":"11_CR19","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare. Communicating sequential processes. CACM, 21(8):666\u2013677, August 1978.","journal-title":"CACM"},{"unstructured":"ISO. Information processing systems \u2014 open systems interconnection \u2014 LOTOS \u2014 a formal description technique based on the temporal ordering of observational behaviour. Technical Report ISO\/TC 97\/SC 21, International Standards Organization, 1987.","key":"11_CR20"},{"unstructured":"C.B. Jones. Systematic program development. In Proc. Symposium on Mathematics and Computer Science, 1986. (also in Software Specification Techniques, pages 89\u2013108).","key":"11_CR21"},{"issue":"1","key":"11_CR22","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/TSE.1985.231535","volume":"11","author":"R.A. Kemmerer","year":"1985","unstructured":"R.A. Kemmerer. Testing formal specifications to detect design errors. IEEE Transactions on Software Engineering, 11(1):32\u201343, January 1985.","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"Requirements for the procurement of safety critical software in defense equipment. U.K. Ministry of Defense, May 1989. Interim Defence Standard 00-55.","key":"11_CR23"},{"issue":"2","key":"11_CR24","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1109\/TSE.1984.5010215","volume":"10","author":"C. Carroll Morgan","year":"1984","unstructured":"C. Carroll Morgan and Bernard A. Sufrin. Specification of the Unix filing system. IEEE Transactions on Software Engineering, 10(2):128\u2013142, March 1984.","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"K. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistencey protocol. In International Symposium on Shared Memory Multiprocessors, 1991.","key":"11_CR25"},{"issue":"3","key":"11_CR26","first-page":"103","volume":"14","author":"C.J. Nix","year":"1988","unstructured":"C.J. Nix and B.P. Collins. The use of software engineering, including the Z notation, in the development of CICS. Quality Assurance, 14(3):103\u2013110, September 1988.","journal-title":"Quality Assurance"},{"issue":"3","key":"11_CR27","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455\u2013495, July 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"11_CR28","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1109\/TSE.1986.6312940","volume":"SE-12","author":"D.L. Parnas","year":"1986","unstructured":"D.L. Parnas and P.C. Clements. A rational design process: How and why to fake it. IEEE Transactions on Software Engineering, SE-12(2):251\u2013257, February 1986.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"11_CR29","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"J.L. Peterson","year":"1977","unstructured":"J.L. Peterson. Petri nets. ACM Computing Surveys, 9(3):223\u2013252, September 1977.","journal-title":"ACM Computing Surveys"},{"issue":"10","key":"11_CR30","first-page":"279","volume":"14","author":"D. Pountain","year":"1989","unstructured":"D. Pountain. Occam II. Byte, 14(10):279\u2013284, October 1989.","journal-title":"Byte"},{"doi-asserted-by":"crossref","unstructured":"Lui Sha and John B. Goodenough. Real-time scheduling theory and Ada.* Computer, pages 53\u201362, April 1990.","key":"11_CR31","DOI":"10.1109\/2.55469"},{"unstructured":"Proceedings of the ACM SIGSOFT'91 Conference on Software for Critical Systems, Software Engineering Notes, Volume 16, Number 5. ACM Press, December 1991.","key":"11_CR32"},{"unstructured":"J.M. Spivey. The Fuzz manual, 1988.","key":"11_CR33"},{"issue":"1","key":"11_CR34","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1049\/sej.1989.0006","volume":"4","author":"J.M. Spivey","year":"1989","unstructured":"J.M. Spivey. An introduction to Z and formal specification. Software Engineering Journal, 4(1):40\u201350, January 1989.","journal-title":"Software Engineering Journal"},{"doi-asserted-by":"crossref","unstructured":"Mary Shaw and James E. Tomayko. Models for undergraduate project courses in software engineering. In Proceedings Fifth SEI Conference on Software Engineering Education, October 1991.","key":"11_CR35","DOI":"10.21236\/ADA241780"},{"issue":"12","key":"11_CR36","first-page":"287","volume":"13","author":"R.M. Stein","year":"1988","unstructured":"R.M. Stein. T800 and counting. Byte, 13(12):287\u2013296, November 1988.","journal-title":"Byte"},{"issue":"9","key":"11_CR37","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J. Wing","year":"1990","unstructured":"J. Wing. A specifier's introduction to formal methods. Computer, 23(9):8\u201326, September 1990.","journal-title":"Computer"},{"unstructured":"A.M. Zaremski. A Larch specification of the Miro Editor. Technical Report CMU-CS-91-111, Carnegie Mellon University, 1991.","key":"11_CR38"},{"issue":"3","key":"11_CR39","first-page":"131","volume":"8","author":"P. Zave","year":"1982","unstructured":"P. Zave. An operational approach to requirements specification for embedded systems. IEEE Trans. on Software Engineering, SE-8(3), 1982. (also in Software Specification Techniques, pages 131\u2013169).","journal-title":"IEEE Trans. on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Software Engineering Education"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55963-9_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:02:19Z","timestamp":1605646939000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55963-9_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540559634","9783540473305"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-55963-9_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}