{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:35:32Z","timestamp":1787564132358,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030613617","type":"print"},{"value":"9783030613624","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-61362-4_10","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T09:02:36Z","timestamp":1603875756000},"page":"187-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Scaling Correctness-by-Construction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8804-7051","authenticated-orcid":false,"given":"Alexander","family":"Kn\u00fcppel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tobias","family":"Runge","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification-The KeY Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification-The KeY Book. Lecture Notes in Computer Science. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0053358","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"R Banach","year":"1998","unstructured":"Banach, R., Poppleton, M.: Retrenchment: an engineering variation on refinement. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 129\u2013147. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/BFb0053358"},{"issue":"4","key":"10_CR4","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00165-005-0073-x","volume":"17","author":"B Beckert","year":"2005","unstructured":"Beckert, B., Schlager, S.: Refinement and retrenchment for programming language data types. Formal Aspects Comput. 17(4), 423\u2013442 (2005)","journal-title":"Formal Aspects Comput."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-92188-2_9","volume-title":"Formal Methods for Components and Objects","author":"A Benveniste","year":"2008","unstructured":"Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200\u2013225. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-92188-2_9"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Passerone, R.: Multi-Viewpoint State Machines for Rich Component Models. Model-Based Design of Heterogeneous Embedded Systems (2009)","DOI":"10.1201\/9781420067859-c15"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P Chalin","year":"2006","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. 4111, pp. 342\u2013363. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11804192_16"},{"key":"10_CR8","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 de Moura","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"10_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs. Comm. ACM 18(8), 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"10_CR10","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1976)","edition":"1"},{"key":"10_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming, 1st edn. Springer, Secaucus (1981). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-5983-1","edition":"1"},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. (CSUR) 44(3), 1\u201358 (2012)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"10","key":"10_CR13","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/MC.2007.364","volume":"40","author":"TA Henzinger","year":"2007","unstructured":"Henzinger, T.A., Sifakis, J.: The discipline of embedded systems design. Computer 40(10), 32\u201340 (2007)","journal-title":"Computer"},{"issue":"10","key":"10_CR14","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11813040_19"},{"key":"10_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5","volume-title":"The Correctness-by-Construction Approach to Programming","author":"DG Kourie","year":"2012","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27919-5"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Lau, K.-K., Tran, C.M.: X-MAN: an MDE tool for component-based system development. In: 2012 38th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 158\u2013165. IEEE (2012)","DOI":"10.1109\/SEAA.2012.32"},{"key":"10_CR19","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998), pp. 404\u2013420. Citeseer (1998)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Muller, P.: Information hiding and visibility in interface specifications. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 385\u2013395. IEEE (2007)","DOI":"10.1109\/ICSE.2007.44"},{"issue":"6","key":"10_CR21","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Programm. Lang. Syst. (TOPLAS)"},{"issue":"10","key":"10_CR22","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying design by contract. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"10_CR23","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall, Upper Saddle River (1994)"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/s00165-003-0003-8","volume":"15","author":"M Oliveira","year":"2003","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: ArcAngel: a Tactic Language For Refinement. Formal Aspects Comput. 15(1), 28\u201347 (2003)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"10_CR25","doi-asserted-by":"publisher","first-page":"1025","DOI":"10.1007\/s11390-017-1779-y","volume":"32","author":"M Ozkaya","year":"2017","unstructured":"Ozkaya, M.: Visual specification and analysis of contract-based software architectures. J. Comput. Sci. Technol. 32(5), 1025\u20131043 (2017). \nhttps:\/\/doi.org\/10.1007\/s11390-017-1779-y","journal-title":"J. Comput. Sci. Technol."},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Ozkaya, M., Kloukinas, C.: Design-by-contract for reusable components and realizable architectures. In: Proceedings of the 17th International ACM SIGSOFT Symposium on Component-Based Software Engineering, pp. 129\u2013138 (2014)","DOI":"10.1145\/2602458.2602463"},{"key":"10_CR27","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1016\/j.entcs.2005.03.018","volume":"130","author":"A Rademaker","year":"2005","unstructured":"Rademaker, A., Braga, C., Sztajnberg, A.: A rewriting semantics for a software architecture description language. Electron. Notes Theor. Comput. Sci. 130, 345\u2013377 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Rawat, D.B., Rodrigues, J.J., Stojmenovic, I.: Cyber-Physical Systems: From Theory to Practice. CRC Press, Boca Raton (2015)","DOI":"10.1201\/b19290"},{"issue":"3","key":"10_CR30","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0164-1212(02)00080-8","volume":"66","author":"RH Reussner","year":"2003","unstructured":"Reussner, R.H., Schmidt, H.W., Poernomo, I.H.: Reliability prediction for component-based software architectures. J. Syst. Softw. 66(3), 241\u2013252 (2003)","journal-title":"J. Syst. Softw."},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Runge, T., Kn\u00fcppel, A., Th\u00fcm, T., Schaefer, I.: Lattice-based information flow control-by-construction for security-by-design. In: FormaliSE 2020. IEEE (2020)","DOI":"10.1145\/3372020.3391565"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-030-16722-6_2","volume-title":"Fundamental Approaches to Software Engineering","author":"T Runge","year":"2019","unstructured":"Runge, T., Schaefer, I., Cleophas, L., Th\u00fcm, T., Kourie, D., Watson, B.W.: Tool support for correctness-by-construction. In: H\u00e4hnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 25\u201342. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-16722-6_2"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-54997-8_25","volume-title":"Formal Methods. FM 2019 International Workshops","author":"T Runge","year":"2020","unstructured":"Runge, T., Th\u00fcm, T., Cleophas, L., Schaefer, I., Watson, B.W.: Comparing correctness-by-construction with post-hoc verification\u2014a qualitative user study. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12233, pp. 388\u2013405. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-54997-8_25"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217\u2013238 (2012)","DOI":"10.3166\/ejc.18.217-238"},{"key":"10_CR35","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"C Szyperski","year":"2002","unstructured":"Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming. Pearson Education, London (2002)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T09:04:46Z","timestamp":1603875886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}