{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:55:04Z","timestamp":1756000504091,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030643539"},{"type":"electronic","value":"9783030643546"}],"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-64354-6_5","type":"book-chapter","created":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:12:03Z","timestamp":1607418723000},"page":"122-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Using Abstract Contracts for Verifying Evolving Features and Their Interactions"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Kn\u00fcppel","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Kr\u00fcger","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Krieter","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Bodden","sequence":"additional","affiliation":[]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,12,4]]},"reference":[{"key":"5_CR1","series-title":"LNCS","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. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"5","key":"5_CR2","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1745312.1745316","volume":"32","author":"S Apel","year":"2010","unstructured":"Apel, S., Hutchins, D.: A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. (TOPLAS) 32(5), 19:1\u201319:33 (2010)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-540-78789-1_2","volume-title":"Software Composition","author":"S Apel","year":"2008","unstructured":"Apel, S., Lengauer, C.: Superimposition: a language-independent approach to software composition. In: Pautasso, C., Tanter, \u00c9. (eds.) SC 2008. LNCS, vol. 4954, pp. 20\u201335. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78789-1_2"},{"key":"5_CR4","unstructured":"Apel, S., K\u00e4stner, C., Lengauer, C.: Featurehouse: language-independent, automated software composition. In: Proceedings International Conference Software Engineering (ICSE), Washington, DC, USA, pp. 221\u2013231. IEEE (2009). ISBN 978-1-4244-3453-4"},{"issue":"11","key":"5_CR5","doi-asserted-by":"publisher","first-page":"1022","DOI":"10.1016\/j.scico.2010.02.001","volume":"75","author":"S Apel","year":"2010","unstructured":"Apel, S., Lengauer, C., M\u00f6ller, B., K\u00e4stner, C.: An algebraic foundation for automatic feature-based program synthesis. Sci. Comput. Program. (SCP) 75(11), 1022\u20131047 (2010)","journal-title":"Sci. Comput. Program. (SCP)"},{"issue":"3","key":"5_CR6","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/j.scico.2010.07.005","volume":"77","author":"S Apel","year":"2012","unstructured":"Apel, S., Kolesnikov, S., Liebig, J., K\u00e4stner, C., Kuhlemann, M., Leich, T.: Access control in feature-oriented programming. Sci. Comput. Program. (SCP) 77(3), 174\u2013187 (2012)","journal-title":"Sci. Comput. Program. (SCP)"},{"key":"5_CR7","series-title":"Concepts and Implementation","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines. Concepts and Implementation. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37521-7"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/TSE.2011.120","volume":"39","author":"S Apel","year":"2013","unstructured":"Apel, S., K\u00e4stner, C., Lengauer, C.: Language-independent and automated software composition: the featurehouse experience. IEEE Trans. Softw. Eng. (TSE) 39(1), 63\u201379 (2013)","journal-title":"IEEE Trans. Softw. Eng. (TSE)"},{"key":"5_CR9","unstructured":"Apel, S., von Rhein, A., Wendler, P., Gr\u00f6\u00dflinger, A., Beyer, D.: Strategies for product-line verification: case studies and experiments. In: Proceedings International Conference Software Engineering (ICSE), Piscataway, pp. 482\u2013491. IEEE (2013). ISBN 978-1-4673-3076-3"},{"key":"5_CR10","unstructured":"Aversano, L., Di Penta, M., Baxter, I.D.: Handling preprocessor-conditioned declarations. In: Proceedings International Working Conference Source Code Analysis and Manipulation (SCAM), Washington, DC, USA, pp. 83\u201392. IEEE, October 2002. ISBN 0-7695-1793-5"},{"key":"5_CR11","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). https:\/\/doi.org\/10.1007\/978-3-662-45231-8_9"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46508-1_8","volume-title":"Transactions on Foundations for Mastering Change I","author":"R Bubel","year":"2016","unstructured":"Bubel, R., et al.: Proof repositories for compositional verification of evolving software systems. In: Steffen, B. (ed.) Transactions on Foundations for Mastering Change I. LNCS, vol. 9960, pp. 130\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46508-1_8"},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S1389-1286(02)00352-3","volume":"41","author":"M Calder","year":"2003","unstructured":"Calder, M., Kolberg, M., Magill, E.H., Reiff-Marganiec, S.: Feature interaction: a critical review and considered forecast. Comput. Netw. 41(1), 115\u2013141 (2003)","journal-title":"Comput. Netw."},{"key":"5_CR14","volume-title":"Generative Programming: Methods, Tools, and Applications","author":"K Czarnecki","year":"2000","unstructured":"Czarnecki, K., Eisenecker, U.: Generative Programming: Methods, Tools, and Applications. ACM\/Addison-Wesley, New York (2000)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Czarnecki, K., Pietroszek, K.: Verifying feature-based model templates against well-formedness OCL constraints. In: Proceedings International Conference Generative Programming and Component Engineering (GPCE), New York, NY, USA, pp. 211\u2013220. ACM (2006)","DOI":"10.1145\/1173706.1173738"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-34026-0_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F Damiani","year":"2012","unstructured":"Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 193\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_15"},{"key":"5_CR17","unstructured":"Damiani, F., Dovland, J., Johnsen, E.B., Owe, O., Sch\u00e4fer, I., Yu, I.C.: A transformational proof system for delta-oriented programming. In: de Almeida, E.S. (ed.) Proceedings International Software Product Line Conference (SPLC), New York, NY, USA, vol. 2, pp. 53\u201360. ACM (2012). ISBN 978-1-4503-1095-6"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Delaware, B., Cook, W.R., Batory, D.: Fitting the pieces together: a machine-checked model of safe composition. In: Proceedings European Software Engineering Conference\/Foundations of Software Engineering (ESEC\/FSE), pp. 243\u2013252. ACM (2009)","DOI":"10.1145\/1595696.1595733"},{"key":"5_CR19","unstructured":"Delaware, B., Cook, W., Batory, D.: Product lines of theorems. In: Proceedings Conference Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), New York, NY, USA, pp. 595\u2013608. ACM (2011). ISBN 978-1-4503-0940-0"},{"key":"5_CR20","unstructured":"Delaware, B.D.S., Oliveira, B.C., Schrijvers, T.: Meta-theory \u00e0 la carte. In: Proceedings Symposium Principles of Programming Languages (POPL), New York, NY, USA, pp. 207\u2013218. ACM (2013). ISBN 978-1-4503-1832-7"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S., Braberman, V.: A foundation for behavioural conformance in software product line architectures. In: Proceedings International Workshop Role of Software Architecture for Testing and Analysis (ROSATEA), New York, NY, USA, pp. 39\u201348. ACM (2006)","DOI":"10.1145\/1147249.1147254"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-22045-6_7","volume-title":"Software Composition","author":"A Gondal","year":"2011","unstructured":"Gondal, A., Poppleton, M., Butler, M.: Composing event-b specifications - case-study experience. In: Apel, S., Jackson, E. (eds.) SC 2011. LNCS, vol. 6708, pp. 100\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22045-6_7"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113\u2013131. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_8"},{"key":"5_CR24","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"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 300\u2013314. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_21"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-540-68237-0_27","volume-title":"FM 2008: Formal Methods","author":"A Harhurin","year":"2008","unstructured":"Harhurin, A., Hartmann, J.: Towards consistent specifications of product families. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 390\u2013405. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_27"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-33314-9_3","volume-title":"Relational and Algebraic Methods in Computer Science","author":"P H\u00f6fner","year":"2012","unstructured":"H\u00f6fner, P., M\u00f6ller, B., Zelend, A.: Foundations of coloring algebra with consequences for feature-oriented programming. In: Kahl, W., Griffin, T.G. (eds.) RAMiCS 2012. LNCS, vol. 7560, pp. 33\u201349. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33314-9_3"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Kang, K.C, Cohen, S.G, Hess, J.A, Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report CMU\/SEI-90-TR-21, Software Engineering Institute (1990)","DOI":"10.21236\/ADA235785"},{"key":"5_CR29","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_CR30","unstructured":"Kolesnikov, S., von Rhein, A., Hunsen, C., Apel, S.: A comparison of product-based, feature-based, and family-based type checking. In: Proceedings International Conference Generative Programming and Component Engineering (GPCE), New York, NY, USA, pp. 115\u2013124. ACM (2013). ISBN 978-1-4503-2373-4"},{"key":"5_CR31","unstructured":"Leavens, G.T., Cheon, Y.: Design by contract with JML, September 2006. http:\/\/www.jmlspecs.org\/jmldbc.pdf"},{"issue":"3","key":"5_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"10","key":"5_CR33","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."},{"issue":"12","key":"5_CR34","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1145\/361598.361623","volume":"15","author":"DL Parnas","year":"1972","unstructured":"Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun. ACM 15(12), 1053\u20131058 (1972)","journal-title":"Commun. ACM"},{"key":"5_CR35","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_CR36","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Kuhlemann, M., Apel, S.: Proof composition for deductive verification of software product lines. In: Proceedings International Workshop Variability-intensive Systems Testing, Validation and Verification (VAST), Washington, pp. 270\u2013277. IEEE Computer (2011)","DOI":"10.1109\/ICSTW.2011.48"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings International Conference Generative Programming and Component Engineering (GPCE), New York, NY, USA, pp. 11\u201320. ACM, September 2012. ISBN 978-1-4503-1129-8","DOI":"10.1145\/2371401.2371404"},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-642-28872-2_18","volume-title":"Fundamental Approaches to Software Engineering","author":"T Th\u00fcm","year":"2012","unstructured":"Th\u00fcm, T., Schaefer, I., Kuhlemann, M., Apel, S., Saake, G.: Applying design by contract to\u00a0feature-oriented programming. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 255\u2013269. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_18"},{"issue":"1","key":"5_CR39","doi-asserted-by":"publisher","first-page":"6: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), 6:1\u20136:45 (2014)","journal-title":"ACM Comput. Surv."},{"key":"5_CR40","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.scico.2012.06.002","volume":"79","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., K\u00e4stner, C., Benduhn, F., Meinicke, J., Saake, G., Leich, T.: FeatureIDE: an extensible framework for feature-oriented software development. Sci. Comput. Program. (SCP) 79, 70\u201385 (2014)","journal-title":"Sci. Comput. Program. (SCP)"},{"key":"5_CR41","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."},{"issue":"1, Part 2","key":"5_CR42","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jlamp.2015.06.007","volume":"85","author":"A von Rhein","year":"2016","unstructured":"von Rhein, A., Th\u00fcm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Logic a Algebraic Methods Program. (JLAMP) 85(1, Part 2), 125\u2013145 (2016)","journal-title":"J. Logic a Algebraic Methods Program. (JLAMP)"},{"issue":"1","key":"5_CR43","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jlamp.2015.06.007","volume":"85","author":"A von Rhein","year":"2016","unstructured":"von Rhein, A., Th\u00fcm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Logic a Algebraic Methods Program. 85(1), 125\u2013145 (2016)","journal-title":"J. Logic a Algebraic Methods Program."}],"container-title":["Lecture Notes in Computer Science","Deductive Software Verification: Future Perspectives"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-64354-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:13:10Z","timestamp":1607418790000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-64354-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030643539","9783030643546"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-64354-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"4 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}