{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:35:23Z","timestamp":1784932523313,"version":"3.55.0"},"publisher-location":"Cham","reference-count":116,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319064093","type":"print"},{"value":"9783319064109","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_4","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"42-61","source":"Crossref","is-referenced-by-count":32,"title":["40 Years of Formal Methods"],"prefix":"10.1007","author":[{"given":"Dines","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book. Cambridge University Press, UK (1996)"},{"key":"4_CR2","volume-title":"Modeling in Event-B: System and Softw. Eng","author":"J.-R. Abrial","year":"2009","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Softw. Eng. Cambridge University Press, UK (2009)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38613-8_1","volume-title":"Integrated Formal Methods","author":"J.-R. Abrial","year":"2013","unstructured":"Abrial, J.-R.: From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 1\u201315. Springer, Heidelberg (2013)"},{"key":"4_CR4","unstructured":"Araki, K., et al. (eds.): IFM 1999\u20132013: Integrated Formal Methods. LNCS, vol.\u00a01945, 2335, 2999, 3771, 4591, 5423, 6496, 7321 and 7940. Springer, Heidelberg (2013)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004), Tool website: http:\/\/research.microsoft.com\/en-us\/projects\/slam","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM\u00a054(6), 81\u201391 (2011), Tool website: http:\/\/research.microsoft.com\/en-us\/projects\/specsharp","DOI":"10.1145\/1953122.1953145"},{"key":"4_CR7","unstructured":"Beki\u010d, H., Bj\u00f8rner, D., Henhapl, W., Jones, C.B., Lucas, P.: A Formal Definition of a PL\/I Subset. Technical Report 25.139, Vienna, Austria (September 20, 1974)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Series: Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"5-6","key":"4_CR9","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. International Journal on Software Tools for Technology Transfer, STTT\u00a09(5-6), 505\u2013525 (2007), Tool website: http:\/\/www.sosy-lab.org\/~dbeyer\/Blast\/index-epfl.php","journal-title":"International Journal on Software Tools for Technology Transfer, STTT"},{"key":"4_CR10","unstructured":"Bj\u00f8rner, D.: Programming Languages: Formal Development of Interpreters and Compilers. In: Morlet, E., Ribbens, D. (eds.) International Computing Symposium 1977, pp. 1\u201321. European ACM, North-Holland Publ. Co., Amsterdam (1977)"},{"key":"4_CR11","unstructured":"Bj\u00f8rner, D. (ed.) Logics of Formal Specification Languages. Computing and Informatics\u00a022(1-2) (2003); This double issue contains the following papers on B, CafeOBJ, CASL, RAISE, TLA+ and Z"},{"key":"4_CR12","unstructured":"Bj\u00f8rner, D.: Software Engineering, Vol.\u00a01: Abstraction and Modelling. Texts in Theoretical Computer Science, the EATCS Series. Springer (2006)"},{"key":"4_CR13","unstructured":"Bj\u00f8rner, D.: Software Engineering, Vol.\u00a02: Specification of Systems and Languages. Texts in Theoretical Computer Science, the EATCS Series. Springer (2006) (Chapters 12\u201314 are primarily authored by Christian Krog Madsen)"},{"key":"4_CR14","unstructured":"Bj\u00f8rner, D.: Software Engineering, Vol.\u00a03: Domains, Requirements and Software Design. Texts in Theoretical Computer Science, the EATCS Series. Springer (2006)"},{"key":"4_CR15","unstructured":"Bj\u00f8rner, D.: Special Double Issue on Formal Methods of Program Development. International Journal of Software and Informatics\u00a03 (2009)"},{"issue":"1","key":"4_CR16","first-page":"1","volume":"1","author":"D. Bj\u00f8rner","year":"2011","unstructured":"Bj\u00f8rner, D.: Believable Software Management. Encyclopedia of Software Engineering\u00a01(1), 1\u201332 (2011)","journal-title":"Encyclopedia of Software Engineering"},{"key":"4_CR17","unstructured":"Bj\u00f8rner, D., et al. (eds.): VDM, FME and FM Symposia 1987\u20132012, LNCS, vol. 252, 328, 428, 551-552, 670, 873, 1051, 1313, 1708-1709, 2021, 2391, 2805, 3582, 4085, 5014, 6664, 7436 (1987\u20132012)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol.\u00a061. Springer, Heidelberg (1978) (This was the first monograph on Meta-IV)","DOI":"10.1007\/3-540-08766-4"},{"key":"4_CR19","unstructured":"Bj\u00f8rner, D., Jones, C.B. (eds.): Formal Specification and Software Development. Prentice-Hall (1982)"},{"key":"4_CR20","series-title":"LNCS","volume-title":"Towards a Formal Description of Ada","year":"1980","unstructured":"Bj\u00f8rner, D., Oest, O.N. (eds.): Towards a Formal Description of Ada. LNCS, vol.\u00a098. Springer, Heidelberg (1980)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1008700623084","volume":"16","author":"N. Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design\u00a016, 227\u2013270 (2000)","journal-title":"Formal Methods in System Design"},{"key":"4_CR22","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. In: Higher-Order Program Analysis (June 2013), http:\/\/hopa.cs.rhul.ac.uk\/files\/proceedings.html"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Jerome Feret, L.M., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"4_CR24","unstructured":"Bowen, J., et al.: Z, B, ZUM, ABZ Meetings, Conferences, Symposia and Workshops, Z Users Workshops: 1986\u20131995; Z, ZB and ABZ Users Meetings: 1996\u20132013. LNCS, vol.\u00a01212, 1493, 1878, 2272, 2651, 3455, 5238, 5977 and 7316 (1986\u20132014)"},{"key":"4_CR25","unstructured":"Burstall, R.M., Landin, P.J.: Programs and their proofs: an algebraic approach. Technical report, DTIC Document (1968)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006), Tool website: http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/index.shtml","DOI":"10.1007\/11804192_16"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004), Tool website: http:\/\/www.cprover.org\/cbmc","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"4_CR28","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000) ISBN 0-262-03270-8"},{"key":"4_CR29","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Oliet, N.M., Meseguer, J., Talcott, C.: Maude 2.6 Manual, Department of Computer Science, University of Illinois and Urbana-Champaign, Urbana-Champaign, Ill. USA (January 2011)"},{"key":"4_CR30","unstructured":"Clemmensen, G., Oest, O.: Formal specification and development of an Ada compiler \u2013 a VDM case study. In: Proc. 7th International Conf. on Software Engineering, Orlando, Florida, March 26-29, pp. 430\u2013440. IEEE (March 1984)"},{"key":"4_CR31","unstructured":"The CML programming language, http:\/\/cml.cs.uchicago.edu"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)","DOI":"10.1007\/b96103"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009), Tool website: http:\/\/research.microsoft.com\/en-us\/projects\/vcc","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35843-2_1","volume-title":"SOFSEM 2013: Theory and Practice of Computer Science","author":"E. Cohen","year":"2013","unstructured":"Cohen, E., Paul, W., Schmaltz, S.: Theory of multi core hypervisor verification. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol.\u00a07741, pp. 1\u201327. Springer, Heidelberg (2013)"},{"key":"4_CR35","unstructured":"CVS: Software Version Control, http:\/\/www.nongnu.org\/cvs\/"},{"key":"4_CR36","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"4_CR37","series-title":"EATCS Series, Monograph in Theoretical Computer Science","volume-title":"Logics of Specification Languages","year":"2008","unstructured":"Bj\u00f8rner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Series, Monograph in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"D\u00fcrr, E.H., van Katwijk, J.: bxcVDM\u2009+\u2009+\u2009exc, A Formal Specification Language for Object Oriented Designs. In: COMP EURO 1992, pp. 214\u2013219. IEEE (May 1992)","DOI":"10.1109\/CMPEUR.1992.218511"},{"key":"4_CR39","volume-title":"Developing Software Using VDM-SL","author":"J. Fitzgerald","year":"1997","unstructured":"Fitzgerald, J., Larsen, P.G.: Developing Software Using VDM-SL. Cambridge University Press, Cambridge (1997)"},{"key":"4_CR40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems \u2013 Practical Tools and Techniques in Software Development","author":"J. Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems \u2013 Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, Cambridge (2009)","edition":"2"},{"key":"4_CR41","unstructured":"Florian, M.: Analysis-Aware Design of Embedded Systems Software. PhD thesis, California Institute of Technology, Pasadena, California (October 2013)"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning Meanings to Programs. In: [103], pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR43","unstructured":"The Frama-C software analysis framework, http:\/\/frama-c.com"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol.\u00a06. World Scientific Publishing Co. Pte. Ltd. (1998)","DOI":"10.1142\/3831"},{"key":"4_CR45","series-title":"The BCS Practitioner Series","volume-title":"The RAISE Specification Language","author":"C.W. George","year":"1992","unstructured":"George, C.W., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead (1992)"},{"key":"4_CR46","series-title":"The BCS Practitioner Series","volume-title":"The RAISE Development Method","author":"C.W. George","year":"1995","unstructured":"George, C.W., Haxthausen, A.E., Hughes, S., Milne, R., Prehn, S., Pedersen, J.S.: The RAISE Development Method. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead (1995)"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Gries, D.: The Science of Programming. Springer (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"issue":"3","key":"4_CR48","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"4_CR49","unstructured":"Havelund, K.: The Fork Calculus - Towards a Logic for Concurrent ML. PhD thesis, DIKU, Department of Computer Science, University of Copenhagen, Denmark (1994)"},{"issue":"4","key":"4_CR50","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, STTT\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer, STTT"},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-40911-4_3","volume-title":"Integrated Formal Methods","author":"A.E. Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Yong, X.: Linking DC together with TRSL. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 25\u201344. Springer, Heidelberg (2000)"},{"key":"4_CR52","unstructured":"Haxthausen, A.E.: Some Approaches for Integration of Specification Techniques. In: INT 2000 \u2013 Integration of Specification Techniques with Applications in Engineering, pp. 33\u201340. Technical University of Berlin, Germany. Dept. of Informatics (2000)"},{"key":"4_CR53","unstructured":"Haxthausen, A.E., Yong, X.: A RAISE Specification Framework and Justification assistant for the Duration Calculus, Saarbr\u00fccken, Dept of Linguistics, Gothenburg University, Sweden (1998)"},{"key":"4_CR54","unstructured":"He, J.: From CSP to Hybrid Systems. In: A Classical Mind. Prentice Hall (1994)"},{"key":"4_CR55","unstructured":"Hehner, E.: The Logic of Programming. Prentice-Hall (1984)"},{"issue":"10","key":"4_CR56","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"Hoare, C.: The Axiomatic Basis of Computer Programming. Communications of the ACM\u00a012(10), 567\u2013583 (1969)","journal-title":"Communications of the ACM"},{"key":"4_CR57","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. Hoare","year":"1972","unstructured":"Hoare, C.: Proof of Correctness of Data Representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"4_CR58","unstructured":"Hoare, C.: Communicating Sequential Processes. C.A.R. Hoare Series in Computer Science. Prentice-Hall International (1985, 2004), Published electronically: http:\/\/www.usingcsp.com\/cspbook.pdf"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Logic verification of ANSI-C code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 131\u2013147. Springer, Heidelberg (2000), Tool website: http:\/\/spinroot.com\/modex","DOI":"10.1007\/10722468_8"},{"key":"4_CR60","volume-title":"The SPIN Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"4_CR61","unstructured":"International Conferences on Formal Engineering Methods, ICFEM (ed.) : LNCS, vol.\u00a02405, 2885, 3308, 3785, 4260, 4789, 5256, 5885, 6447 and 8144, IEEE Computer Society Press and Springer Years 2002\u20132013: IEEE, Years 2002\u20132013"},{"key":"4_CR62","unstructured":"ITU-T. CCITT Recommendation Z.120: Message Sequence Chart (MSC) (1992, 1996, 1999)"},{"key":"4_CR63","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006) ISBN 0-262-10114-9"},{"key":"4_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011), Tool website: http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast"},{"key":"4_CR65","series-title":"Object Technology Series","volume-title":"The Unified Software Development Process","author":"I. Jacobson","year":"1999","unstructured":"Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Object Technology Series. Addison\u2013Wesley, Addison Wesley Longman, Inc., One Jacob Way, Reading (1999)"},{"key":"4_CR66","unstructured":"Jones, C.B.: Software Development: A Rigorous Approach. Prentice-Hall (1980)"},{"key":"4_CR67","unstructured":"Jones, C.B.: Systematic Software Development \u2014 Using VDM, 2nd edn. Prentice-Hall (1989)"},{"key":"4_CR68","unstructured":"Jones, N.D., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. C.A.R.Hoare Series in Computer Science. Prentice Hall International (1993)"},{"key":"4_CR69","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: A gentle introduction. Theoretical Computer Science\u00a0173, 445\u2013484 (1997), Tool website: http:\/\/homepages.inf.ed.ac.uk\/dts\/eml","journal-title":"Theoretical Computer Science"},{"key":"4_CR70","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (June 2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"4_CR71","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (June 2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"4_CR72","volume-title":"The Art of Computer Programming, Fundamental Algorithms","author":"D. Knuth","year":"1968","unstructured":"Knuth, D.: The Art of Computer Programming, Fundamental Algorithms, vol.\u00a01. Addison-Wesley, Reading (1968)"},{"key":"4_CR73","volume-title":"The Art of Computer Programming, Seminumerical Algorithms","author":"D. Knuth","year":"1969","unstructured":"Knuth, D.: The Art of Computer Programming, Seminumerical Algorithms, vol.\u00a02. Addison-Wesley, Reading (1969)"},{"key":"4_CR74","volume-title":"The Art of Computer Programming, Searching & Sorting","author":"D. Knuth","year":"1973","unstructured":"Knuth, D.: The Art of Computer Programming, Searching & Sorting, vol.\u00a03. Addison-Wesley, Reading (1973)"},{"key":"4_CR75","unstructured":"Lakos, C., et al. (eds.): SEFM: International IEEE Conferences on Software Engineering and Formal Methods, SEFM 2002\u20132013. IEEE Computer Society Press (2003-2013)"},{"key":"4_CR76","volume-title":"Specifying Systems","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison\u2013Wesley, Boston (2002)"},{"issue":"4","key":"4_CR77","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P.J. Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal\u00a06(4), 308\u2013320 (1964)","journal-title":"The Computer Journal"},{"issue":"2","key":"4_CR78","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/363744.363749","volume":"8","author":"P.J. Landin","year":"1965","unstructured":"Landin, P.J.: Correspondence between ALGOL 60 and Church\u2019s Lambda-notation: part i. Communications of the ACM\u00a08(2), 89\u2013101 (1965)","journal-title":"Communications of the ACM"},{"key":"4_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010), Tool website: http:\/\/research.microsoft.com\/en-us\/projects\/dafny"},{"key":"4_CR80","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive Systems: Specifications. Addison Wesley (1991)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"4_CR81","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive Systems: Safety. Addison Wesley (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"4","key":"4_CR82","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive Functions of Symbolic Expressions and Their Computation by Machines, Part I. Communications of the ACM\u00a03(4), 184\u2013195 (1960)","journal-title":"Communications of the ACM"},{"key":"4_CR83","unstructured":"McCarthy, J.: Towards a Mathematical Science of Computation. In: Popplewell, C. (ed.) IFIP World Congress Proceedings, pp. 21\u201328 (1962)"},{"key":"4_CR84","unstructured":"Meyer, B.: Eiffel: The Language, 2nd revised edn., 300 pages. Prentice Hall PTR, Upper Sadle River (1992) (Amazon price: US $ 47.00)"},{"key":"4_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"4_CR86","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. The MIT Press, Cambridge (1990)"},{"key":"4_CR87","unstructured":"Miller, A., Paul, W.: Computer Architecture, Complexity and Correctness. Springer (2000)"},{"key":"4_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR89","unstructured":"The OCaml programming language, http:\/\/ocaml.org"},{"key":"4_CR90","unstructured":"Oest, O.N.: Vdm from research to practice (invited paper). In: IFIP Congress, pp. 527\u2013534 (1986)"},{"key":"4_CR91","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference, Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)"},{"key":"4_CR92","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)"},{"key":"4_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-69149-5_2","volume-title":"Verified Software: Theories, Tools, Experiments","author":"W. Paul","year":"2008","unstructured":"Paul, W.: Towards a Worldwide Verification Technology. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 19\u201325. Springer, Heidelberg (2008)"},{"key":"4_CR94","unstructured":"Paulson, L.C.: ML for the Working Programmer. Cambridge University Press (1991)"},{"key":"4_CR95","unstructured":"The Python programming language, http:\/\/www.python.org"},{"key":"4_CR96","doi-asserted-by":"crossref","unstructured":"Reisig, W.: Abstract State Machines for the Classroom. In: [37], pp. 15\u201346. Springer (2008)","DOI":"10.1007\/978-3-540-74107-7_2"},{"key":"4_CR97","unstructured":"Reisig, W.: Petrinetze: Modellierungstechnik, Analysemethoden, Fallstudien. Leitf\u00e4den der Informatik, 1st edn., June 15, 248 pages. Vieweg+Teubner (2010) ISBN 978-3-8348-1290-2"},{"key":"4_CR98","doi-asserted-by":"crossref","unstructured":"Reisig, W.: Understanding Petri Nets Modeling Techniques, Analysis Methods, Case Studies, 230+XXVII pages. Springer (2013) (145 illus)","DOI":"10.1007\/978-3-642-33278-4"},{"key":"4_CR99","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference, vol.\u00a02, pp. 717\u2013740. ACM (1972)","DOI":"10.1145\/800194.805852"},{"key":"4_CR100","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice Hall PTR (1981)"},{"key":"4_CR101","doi-asserted-by":"crossref","unstructured":"Sannella, D., Tarlecki, A.: Foundations of Algebraic Semantcs and Formal Software Development. Monographs in Theoretical Computer Science. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-17336-3"},{"key":"4_CR102","unstructured":"The Scala programming language, http:\/\/www.scala-lang.org"},{"key":"4_CR103","unstructured":"Schwartz, J.: Mathematical Aspects of Computer Science. In: Proc. of Symp. in Appl. Math. American Mathematical Society, Rhode Island (1967)"},{"key":"4_CR104","unstructured":"Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. In: Computers and Automata. Microwave Research Inst. Symposia, vol.\u00a021, pp. 19\u201346 (1971)"},{"key":"4_CR105","unstructured":"Sestoft, P.: Java Precisely, July 25. The MIT Press (2002)"},{"key":"4_CR106","unstructured":"Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial, Computer Science Laboratory, SRI International, Menlo Park, CA (February1993); Also appears in Tutorial Notes, Formal Methods Europe 1993: Industrial-Strength Formal Methods, Odense, Denmark, pp. 357\u2013406 (April 1993)"},{"key":"4_CR107","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Prover Guide, Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)"},{"key":"4_CR108","unstructured":"Sommerville, I.: Software Engineering. Addison-Wesley (1982)"},{"key":"4_CR109","unstructured":"Static analysers: Semmle, http:\/\/www.semmle.com , Coverity: http:\/\/www.coverity.com , CodeSonar: http:\/\/www.grammatech.com\/codesonar , KlocWork: http:\/\/www.klocwork.com , etc."},{"key":"4_CR110","unstructured":"Thompson, S.: Haskell: The Craft of Functional Programming, 2nd edn., March 29, 512 pages. Addison Wesley (1999) ISBN 0201342758"},{"issue":"2","key":"4_CR111","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng.\u00a010(2), 203\u2013232 (2003), Tool website: http:\/\/javapathfinder.sourceforge.net","journal-title":"Autom. Softw. Eng."},{"key":"4_CR112","doi-asserted-by":"crossref","unstructured":"Whysall, P.J., McDermid, J.A.: An approach to object-oriented specification using Z. In: Nicholls, J.E. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing, pp. 193\u2013215. Springer (1991)","DOI":"10.1007\/978-1-4471-3540-1_13"},{"issue":"4","key":"4_CR113","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J. Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal Methods: Practice and Experience. ACM Computing Surveys\u00a041(4), 19 (2009)","journal-title":"ACM Computing Surveys"},{"key":"4_CR114","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)"},{"key":"4_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-39721-9_5","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","author":"N. Zhan","year":"2013","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol.\u00a08050, pp. 207\u2013281. Springer, Heidelberg (2013)"},{"key":"4_CR116","unstructured":"Zhou, C.C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real\u2013time Systems. Monographs in Theoretical Computer Science. An EATCS Series\u2013Verlag. Springer (2004)"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:34:14Z","timestamp":1746189254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_4"}},"subtitle":["Some Obstacles and Some Possibilities?"],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":116,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}