{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:35Z","timestamp":1792264655990,"version":"4.4.0"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031081651","type":"print"},{"value":"9783031081668","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_5","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"80-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Re-CorC-ing KeY: Correct-by-Construction Software Development Based on\u00a0KeY"],"prefix":"10.1007","author":[{"given":"Tabea","family":"Bordis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Loek","family":"Cleophas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Kittelmann","sequence":"additional","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"}]},{"given":"Bruce W.","family":"Watson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. 1st edn. (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"5_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification - The KeY Book (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-07317-0_5","volume-title":"Formal Methods for Executable Software Models","author":"A Amighi","year":"2014","unstructured":"Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172\u2013216. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_5"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines (2013)","DOI":"10.1007\/978-3-642-37521-7"},{"issue":"3","key":"5_CR6","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/s00165-008-0070-y","volume":"21","author":"RJ Back","year":"2009","unstructured":"Back, R.J.: Invariant based programming: basic approach and teaching experiences. Formal Aspects Comput. 21(3), 227\u2013244 (2009). https:\/\/doi.org\/10.1007\/s00165-008-0070-y","journal-title":"Formal Aspects Comput."},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-73770-4_4","volume-title":"Tests and Proofs","author":"R-J Back","year":"2007","unstructured":"Back, R.-J., Eriksson, J., Myreen, M.: Testing and verifying invariant based programs in the SOCOS environment. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 61\u201378. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73770-4_4"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer Science & Business Media (2012). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"5_CR9","unstructured":"Barnes, J.G.P.: High Integrity Software: The Spark Approach to Safety and Security. Pearson Education (2003)"},{"issue":"6","key":"5_CR10","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1109\/TSE.2004.23","volume":"30","author":"D Batory","year":"2004","unstructured":"Batory, D., Sarvela, J.N., Rauschmayer, A.: Scaling step-wise refinement. IEEE Trans. Softw. Eng. 30(6), 355\u2013371 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Bordis, T., Runge, T., Schaefer, I.: Correctness-by-construction for feature-oriented software product lines. In: Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pp. 22\u201334 (2020)","DOI":"10.1145\/3425898.3426959"},{"issue":"10","key":"5_CR12","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A Borgida","year":"1995","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785\u2013798 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-18070-5_5","volume-title":"Formal Verification of Object-Oriented Software","author":"D Bruns","year":"2011","unstructured":"Bruns, D., Klebanov, V., Schaefer, I.: Verification of software product lines with delta-oriented slicing. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 61\u201375. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_5"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","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. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35"},{"issue":"5","key":"5_CR16","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1109\/TSE.2010.83","volume":"37","author":"I Crnkovic","year":"2010","unstructured":"Crnkovic, I., Sentilles, S., Vulgarakis, A., Chaudron, M.R.: A classification framework for software component models. IEEE Trans. Softw. Eng. 37(5), 593\u2013615 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/3-540-36208-8_2","volume-title":"Object-Oriented Technology ECOOP 2002 Workshop Reader","author":"K Czarnecki","year":"2002","unstructured":"Czarnecki, K., \u00d8sterbye, K., V\u00f6lter, M.: Generative programming. In: Hern\u00e1ndez, J., Moreira, A. (eds.) ECOOP 2002. LNCS, vol. 2548, pp. 15\u201329. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36208-8_2"},{"issue":"8","key":"5_CR19","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, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"5_CR20","unstructured":"Dijkstra, E.W.: A Discipline of Programming. 1st edn. Prentice Hall PTR (1976)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Gries, D.: The Science of Programming. 1st edn. (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"5_CR22","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Component-based Synthesis Applied to Bitvector Programs"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-34026-0_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"R H\u00e4hnle","year":"2012","unstructured":"H\u00e4hnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 32\u201346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_4"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1023\/B:AUSE.0000049208.84702.84","volume":"12","author":"RJ Hall","year":"2005","unstructured":"Hall, R.J.: Fundamental nonmodularity in electronic mail. Autom. Softw. Eng. 12(1), 41\u201379 (2005)","journal-title":"Autom. Softw. Eng."},{"issue":"1","key":"5_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0167-6423(92)90035-A","volume":"18","author":"M Heisel","year":"1992","unstructured":"Heisel, M.: Formalizing and implementing Gries\u2019 program development method in dynamic logic. Sci. Comput. Program. 18(1), 107\u2013137 (1992)","journal-title":"Sci. Comput. Program."},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304\u2013311. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_21"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-61362-4_10","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"A Kn\u00fcppel","year":"2020","unstructured":"Kn\u00fcppel, A., Runge, T., Schaefer, I.: Scaling correctness-by-construction. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 187\u2013207. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_10"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-030-03427-6_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"A Kn\u00fcppel","year":"2018","unstructured":"Kn\u00fcppel, A., Th\u00fcm, T., Padylla, C., Schaefer, I.: Scalability of deductive verification depends on method call treatment. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 159\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_15"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming (2012)","DOI":"10.1007\/978-3-642-27919-5"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., M\u00fcller, P.: Information Hiding and Visibility in Interface Specifications, pp. 385\u2013395 (2007)","DOI":"10.1109\/ICSE.2007.44"},{"key":"5_CR31","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). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"5","key":"5_CR32","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"KRM Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24(5), 491\u2013553 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"5_CR33","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"5_CR34","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0164-1212(88)90022-2","volume":"8","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Eiffel: a language and environment for software engineering. J. Syst. Softw. 8(3), 199\u2013246 (1988)","journal-title":"J. Syst. Softw."},{"issue":"10","key":"5_CR35","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u2018design by contract\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"5_CR36","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall (1998)"},{"issue":"1","key":"5_CR37","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. Form. Asp. Comput. 15(1), 28\u201347 (2003)","journal-title":"Form. Asp. Comput."},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-02654-1_13","volume-title":"Software Language Engineering","author":"DJ Pearce","year":"2013","unstructured":"Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238\u2013248. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_13"},{"issue":"1","key":"5_CR39","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M Plath","year":"2001","unstructured":"Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53\u201384 (2001)","journal-title":"Sci. Comput. Program."},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles and Techniques (2005)","DOI":"10.1007\/3-540-28901-1"},{"issue":"6","key":"5_CR41","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1145\/2980983.2908093","volume":"51","author":"N Polikarpova","year":"2016","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. ACM SIGPLAN Not. 51(6), 522\u2013538 (2016)","journal-title":"ACM SIGPLAN Not."},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-91550-6_8","volume-title":"Formal Methods Teaching","author":"T Runge","year":"2021","unstructured":"Runge, T., Bordis, T., Th\u00fcm, T., Schaefer, I.: Teaching correctness-by-construction and post-hoc verification \u2013 the online experience. In: Ferreira, J.F., Mendes, A., Menghi, C. (eds.) FMTea 2021. LNCS, vol. 13122, pp. 101\u2013116. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-91550-6_8"},{"key":"5_CR43","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). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_2"},{"key":"5_CR44","unstructured":"Runge, T., Servetto, M., Potanin, A., Schaefer, I.: Traits for Correct-by-Construction Programming. To be published (2021)"},{"key":"5_CR45","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., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P., Delmas, D. (eds.) FM 2019. LNCS, vol. 12233, pp. 388\u2013405. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54997-8_25"},{"key":"5_CR46","doi-asserted-by":"crossref","unstructured":"Sametinger, J.: Software Engineering with Reusable Components. Springer Science & Business Media (1997)","DOI":"10.1007\/978-3-662-03345-6"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-30942-8_20","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"D Steinh\u00f6fel","year":"2019","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 319\u2013336. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_20"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-58156-1_24","volume-title":"Automated Deduction \u2014 CADE-12","author":"M Stickel","year":"1994","unstructured":"Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libraries. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 341\u2013355. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_24"},{"key":"5_CR49","unstructured":"Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming. Pearson Education (2002)"},{"issue":"1","key":"5_CR50","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 1\u201345 (2014)","journal-title":"ACM Comput. Surv."},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.jss.2019.01.044","volume":"152","author":"T Th\u00fcm","year":"2019","unstructured":"Th\u00fcm, T., Kn\u00fcppel, A., Kr\u00fcger, S., Bolle, S., Schaefer, I.: Feature-oriented contract composition. J. Syst. Softw. 152, 83\u2013107 (2019)","journal-title":"J. Syst. Softw."},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, p. 11\u201320. GPCE 2012, Association for Computing Machinery, NY (2012)","DOI":"10.1145\/2371401.2371404"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-662-46681-0_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Tschannen","year":"2015","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566\u2013580. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53"},{"key":"5_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/978-3-319-47166-2_52","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"BW Watson","year":"2016","unstructured":"Watson, B.W., Kourie, D.G., Schaefer, I., Cleophas, L.: Correctness-by-construction and post-hoc verification: a marriage of convenience? In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 730\u2013748. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_52"},{"key":"5_CR55","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic, and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:38:00Z","timestamp":1656891480000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}