{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:28:57Z","timestamp":1743035337599,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319465074"},{"type":"electronic","value":"9783319465081"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46508-1_5","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T21:53:39Z","timestamp":1474494819000},"page":"71-89","source":"Crossref","is-referenced-by-count":1,"title":["Verified Change"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Rahul","family":"Kumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,23]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0004-3702(84)90008-0","volume":"23","author":"JF Allen","year":"1984","unstructured":"Allen, J.F.: Towards a general theory of action and time. Artif. Intell. 23, 123\u2013154 (1984)","journal-title":"Artif. Intell."},{"key":"5_CR3","unstructured":"ANTLR. http:\/\/www.antlr.org"},{"key":"5_CR4","series-title":"Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Texts in Computer Science. Springer, New York (1998)"},{"key":"5_CR5","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4\u00a0% false alarms. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 35\u201342. FMCAD Inc. (2010)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08766-4","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bj\u00f8rner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978). doi: 10.1007\/3-540-08766-4"},{"key":"5_CR7","volume-title":"Formal Specification and Software Development","author":"D Bj\u00f8rner","year":"1982","unstructured":"Bj\u00f8rner, D., Jones, C.B.: Formal Specification and Software Development. Prentice Hall International, Englewood Cliffs (1982). ISBN: 0-13-880733-7"},{"key":"5_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364, Wroc\u0142aw, Poland, August 2011"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-662-45231-8_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"R Bubel","year":"2014","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45231-8_9"},{"key":"5_CR10","unstructured":"Coq. https:\/\/coq.inria.fr"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura De","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"5_CR12","unstructured":"Eiffel. http:\/\/www.eiffel.com"},{"key":"5_CR13","unstructured":"Europa Clipper Mission. http:\/\/www.jpl.nasa.gov\/missions\/europa-mission"},{"key":"5_CR14","volume-title":"Validated Designs for Object-Oriented Systems","author":"J Fitzgerald","year":"2005","unstructured":"Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-Oriented Systems. Springer, London (2005)"},{"key":"5_CR15","unstructured":"Fortress. http:\/\/java.net\/projects\/projectfortress"},{"key":"5_CR16","series-title":"The BCS Practitioner Series","volume-title":"The RAISE Specification Language","author":"C George","year":"1992","unstructured":"George, C., Haff, P., Havelund, K., Haxthausen, A., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead (1992)"},{"key":"5_CR17","series-title":"Monographs in Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-3-540-74107-7_7","volume-title":"Logics of Specification Languages","author":"C George","year":"2008","unstructured":"George, C., Haxthausen, A.: The logic of the RAISE specification language. In: Bj\u00f8rner, D., Henson, M. (eds.) Logics of Specification Languages. Monographs in Theoretical Computer Science, pp. 349\u2013399. Springer, Heidelberg (2008)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference, pp. 466\u2013471. ACM (2009)","DOI":"10.1145\/1629911.1630034"},{"issue":"3","key":"5_CR19","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1016\/j.tcs.2005.06.017","volume":"343","author":"Y Gurevich","year":"2005","unstructured":"Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theor. Comput. Sci. 343(3), 370\u2013412 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40615-7_1","volume-title":"Formal Methods for Components and Objects","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Giachino, E., H\u00e4hnle, R., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 1\u201337. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40615-7_1"},{"key":"5_CR21","unstructured":"Haskell. http:\/\/www.haskell.org\/haskellwiki\/Haskell"},{"key":"5_CR22","unstructured":"Havelund, K.: Closing the gap between specification, programming: VDM $$^{++}$$ + + and Scala. In: Korovina, M., Voronkov, A. (eds.) HOWARD-60: Higher-Order Workshop on Automated Runtime Verification and Debugging, EasyChair Proceedings, Manchester, vol. 1, December 2011"},{"issue":"4","key":"5_CR23","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transf. STTT 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf. STTT"},{"issue":"1","key":"5_CR24","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/s10009-002-0080-7","volume":"4","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8\u201320 (2002)","journal-title":"STTT"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187\u2013196. Springer, Heidelberg (1986). doi: 10.1007\/3-540-16442-1_14"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-10181-1_4","volume-title":"Integrated Formal Methods","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., K\u00e4sdorf, S., H\u00e4hnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55\u201370. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-10181-1_4"},{"key":"5_CR27","volume-title":"The Spin Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"5_CR28","unstructured":"Isabelle. https:\/\/isabelle.in.tum.de"},{"key":"5_CR29","volume-title":"Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D., Abstractions, S.: Logic, Language, and Analysis. The MIT Press, Cambridge (2012)"},{"key":"5_CR30","unstructured":"JML. http:\/\/www.eecs.ucf.edu\/leavens\/JML"},{"key":"5_CR31","volume-title":"Systematic Software Development using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Upper Saddle River (1990). ISBN: 0-13-880733-7"},{"volume-title":"Case Studies in Systematic Software Development","year":"1990","key":"5_CR32","unstructured":"Jones, C.B., Shaw, R.C. (eds.): Case Studies in Systematic Software Development. Prentice Hall International, Upper Saddle River (1990). ISBN: 0-13-880733-7"},{"key":"5_CR33","unstructured":"K. http:\/\/www.theklanguage.com"},{"key":"5_CR34","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 173, 445\u2013484 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_54"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_20"},{"volume-title":"The Definition of Standard ML","year":"1997","key":"5_CR37","unstructured":"Milner, R., Tofte, M., Harper, R. (eds.): The Definition of Standard ML. MIT Press, Cambridge (1997). ISBN: 0-262-63181-4"},{"key":"5_CR38","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, New York (1994)","edition":"2"},{"key":"5_CR39","unstructured":"OCaml. http:\/\/caml.inria.fr\/ocaml\/index.en.html"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-16612-9_5","volume-title":"Runtime Verification","author":"M Odersky","year":"2010","unstructured":"Odersky, M.: Contracts for Scala. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 51\u201357. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16612-9_5"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi: 10.1007\/3-540-55602-8_217"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S., P\u0103s\u0103reanu, C.S.: Differential symbolic execution. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 226\u2013237. ACM (2008)","DOI":"10.1145\/1453101.1453131"},{"key":"5_CR43","unstructured":"PVS. http:\/\/pvs.csl.sri.com"},{"key":"5_CR44","unstructured":"Python. http:\/\/www.python.org"},{"key":"5_CR45","unstructured":"Scala. http:\/\/www.scala-lang.org"},{"key":"5_CR46","unstructured":"Spec#. http:\/\/research.microsoft.com\/en-us\/projects\/specsharp"},{"key":"5_CR47","volume-title":"Understanding Z: A Specification Language and Its Formal Semantics","author":"JM Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, New York (1988)"},{"key":"5_CR48","unstructured":"Steffen, B.: LNCS transactions on foundations for mastering change: preliminary manifesto. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS. Theoretical Computer Science and General Issues, vol. 8803, pp. 514\u2013517. Springer, Heidelberg (2014)"},{"key":"5_CR49","unstructured":"SysML. http:\/\/www.omgsysml.org"},{"key":"5_CR50","unstructured":"UML. http:\/\/www.uml.org"},{"key":"5_CR51","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM (CACM) 14, 221\u2013227 (1971)","journal-title":"Commun. ACM (CACM)"},{"key":"5_CR52","volume-title":"Using Z. Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. Prentice-Hall, New York (1996)"}],"container-title":["Lecture Notes in Computer Science","Transactions on Foundations for Mastering Change I"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46508-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:24:30Z","timestamp":1498332270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46508-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465074","9783319465081"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46508-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}