{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:15:15Z","timestamp":1771485315284,"version":"3.50.1"},"publisher-location":"Cham","reference-count":121,"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_1","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Who Carries the Burden of Modularity?"],"prefix":"10.1007","author":[{"given":"Dilian","family":"Gurov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"1_CR2","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":"1_CR3","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 - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-10373-5_20","volume-title":"Formal Methods and Software Engineering","author":"W Ahrendt","year":"2009","unstructured":"Ahrendt, W., Dylla, M.: A verification system for distributed objects with asynchronous method calls. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 387\u2013406. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_20"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W., Petrova, E.: Automated verification of a small hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 40\u201354. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_3"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comp. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comp. Sci."},{"issue":"2\u20133","key":"1_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"key":"1_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines: Concepts and Implementation","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D.S., 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":"3","key":"1_CR9","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359\u2013385 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR10","unstructured":"Arbab, F., Cruz-Filipe, L., Jongmans, S., Montesi, F.: Connectors meet choreographies. CoRR, abs\/1804.08976 (2018)"},{"issue":"6","key":"1_CR11","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R Back","year":"1988","unstructured":"Back, R.: A calculus of refinements for program derivations. Acta Informatica 25(6), 593\u2013624 (1988)","journal-title":"Acta Informatica"},{"key":"1_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51803-7","volume-title":"Temporal Logic in Specification","year":"1987","unstructured":"Banieqbal, B., Barringer, H., Pnueli, A. (eds.): Temporal Logic in Specification. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-51803-7"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Composing communicating systems, synchronously. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 39\u201359. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_3"},{"issue":"12","key":"1_CR14","first-page":"2059","volume":"14","author":"DS Batory","year":"2008","unstructured":"Batory, D.S., B\u00f6rger, E.: Modularizing theorems for software product lines: the Jbook case study. J. Univers. Comput. Sci. 14(12), 2059\u20132082 (2008)","journal-title":"J. Univers. Comput. Sci."},{"key":"1_CR15","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA, Version 1.4 (2010)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Proceedings of the 7th Conference on Systems Software Verification. EPTCS, vol. 102, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M.: Modular verification of JML contracts using bounded model checking. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 60\u201380. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"1_CR18","unstructured":"Beckert, B., Klebanov, V.: Proof reuse for deductive program verification. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM), Beijing, China, pp. 77\u201386. IEEE Computer Society (2004)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-319-91908-9_16","volume-title":"Computing and Software Science","author":"A Benveniste","year":"2019","unstructured":"Benveniste, A., Caillaud, B., Elmqvist, H., Ghorbal, K., Otter, M., Pouzet, M.: Multi-mode dae models - challenges, theory and implementation. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 283\u2013310. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_16"},{"key":"1_CR20","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). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_9"},{"key":"1_CR21","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development-Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development-Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Beyer, D., Kanav, S.: An interface theory for program verification (position paper). In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 168\u2013186. Springer (October 2020)","DOI":"10.1007\/978-3-030-61362-4_9"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-47166-2_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195\u2013211. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: survey and unifying component framework. In Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 143\u2013167. Springer (October 2020)","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"1_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12\u201314 January 2005, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1040305.1040327"},{"issue":"6","key":"1_CR29","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/390016.808445","volume":"10","author":"RS Boyer","year":"1975","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT\u2013a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not. 10(6), 234\u2013245 (1975)","journal-title":"ACM SIGPLAN Not."},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-36946-9_10","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"J Boyland","year":"2013","unstructured":"Boyland, J.: Fractional permissions. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 270\u2013288. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_10"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-77351-1_4","volume-title":"Software Composition","author":"M Bravetti","year":"2007","unstructured":"Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34\u201350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77351-1_4"},{"issue":"3","key":"1_CR32","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes, S., O\u2019Hearn, P.W.: Concurrent separation logic. SIGLOG News 3(3), 47\u201365 (2016)","journal-title":"SIGLOG News"},{"key":"1_CR33","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"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24312-2_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Bubel","year":"2015","unstructured":"Bubel, R., Din, C.C., H\u00e4hnle, R., Nakata, K.: A dynamic logic with traces and coinduction. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 307\u2013322. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_21"},{"key":"1_CR35","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":"1_CR36","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 845\u2013911. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"1_CR37","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-level Guidance for Mathematical Reasoning","author":"A Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press, Cambridge (2005)"},{"key":"1_CR38","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing, vol. 1974, pp. 308\u2013312. Elsevier\/North-Holland (1974)"},{"issue":"2","key":"1_CR39","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/2220365.2220367","volume":"34","author":"M Carbone","year":"2012","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-21461-5_1","volume-title":"Formal Techniques for Distributed Systems","author":"G Castagna","year":"2011","unstructured":"Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party sessions. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE-2011. LNCS, vol. 6722, pp. 1\u201328. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_1"},{"key":"1_CR41","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: A TLA+ proof system. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, Doha, Qatar, vol. 418. CEUR-WS.org (2008)"},{"key":"1_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36946-9_3","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"D Clarke","year":"2013","unstructured":"Clarke, D., \u00d6stlund, J., Sergey, I., Wrigstad, T.: Ownership types: a survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 15\u201358. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_3"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Coto, A., Guanciale, R., Tuosto, E.: On testing message-passing components. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 22\u201338. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_2"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Language, Los Angeles, pp. 238\u2013252. ACM Press, New York (January 1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Damiani, F., Lienhardt, M., Paolini, L.: On slicing software product line signatures. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 81\u2013102. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_5"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, Vienna, Austria, 10\u201314 September 2001, pp. 109\u2013120. ACM (2001)","DOI":"10.1145\/503209.503226"},{"issue":"5","key":"1_CR48","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1145\/3122848","volume":"50","author":"F de Boer","year":"2017","unstructured":"de Boer, F., et al.: A survey of active object languages. ACM Comput. Surv. 50(5), 761\u20137639 (2017). Article 76","journal-title":"ACM Comput. Surv."},{"issue":"6","key":"1_CR49","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10817-017-9426-4","volume":"62","author":"S De Gouw","year":"2019","unstructured":"De Gouw, S., De Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. J. Autom. Reasoning 62(6), 93\u2013126 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9426-4","journal-title":"J. Autom. Reasoning"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Delaware, B., Cook, W.R., Batory, D.S.: Product lines of theorems. In: Lopes, C.V., Fisher, K. (eds.) Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, Portland, OR, USA, pp. 595\u2013608. ACM (2011)","DOI":"10.1145\/2048066.2048113"},{"issue":"8","key":"1_CR51","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2005.4.8.a1","volume":"4","author":"W Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: lightweight ownership for JML. J. Object Technol. 4(8), 5\u201332 (2005)","journal-title":"J. Object Technol."},{"key":"1_CR52","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66902-1_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"CC Din","year":"2017","unstructured":"Din, C.C., H\u00e4hnle, R., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Locally abstract, globally concrete semantics of concurrent programming languages. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 22\u201343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_2"},{"issue":"3","key":"1_CR54","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27(3), 551\u2013572 (2015)","journal-title":"Formal Aspects Comput."},{"issue":"10","key":"1_CR55","doi-asserted-by":"publisher","first-page":"915","DOI":"10.1016\/j.scico.2010.09.006","volume":"76","author":"J Dovland","year":"2011","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915\u2013941 (2011)","journal-title":"Sci. Comput. Program."},{"key":"1_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-15648-8_7","volume-title":"Logics of Programs","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A.: Automata, tableaux, and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79\u201388. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_7"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Savannah, GA, USA, pp. 315\u2013327. ACM (2009)","DOI":"10.1145\/1480881.1480922"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Abstraction and genericity in Why3. In: Margaria, T., Steffen, B., (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 122\u2013142. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_7"},{"issue":"2","key":"1_CR59","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0167-6423(84)90018-2","volume":"4","author":"R Gerth","year":"1984","unstructured":"Gerth, R., de Roever, W.P.: A proof system for concurrent ADA programs. Sci. Comput. Program. 4(2), 159\u2013204 (1984)","journal-title":"Sci. Comput. Program."},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Dwyer, M.B., Tip, F. (eds.) Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA, Toronto, Canada, pp. 23\u201333. ACM (2011)","DOI":"10.1145\/2001420.2001424"},{"issue":"1\u20133","key":"1_CR61","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.scico.2004.05.014","volume":"55","author":"G G\u00f6\u00dfler","year":"2005","unstructured":"G\u00f6\u00dfler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1\u20133), 161\u2013183 (2005)","journal-title":"Sci. Comput. Program."},{"key":"1_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"1_CR63","series-title":"Texts and Monographs in Computer Science","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. Texts and Monographs in Computer Science. Springer, New York (1981). https:\/\/doi.org\/10.1007\/978-1-4612-5983-1"},{"key":"1_CR64","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.tcs.2013.02.006","volume":"480","author":"D Gurov","year":"2013","unstructured":"Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. Theoret. Comput. Sci. 480, 69\u2013103 (2013)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"key":"1_CR66","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":"1_CR67","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic (Foundations of Computing)","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic (Foundations of Computing). MIT Press, Cambridge (2000)"},{"key":"1_CR68","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI 1973, pp. 235\u2013245. Morgan Kaufmann Publishers Inc. (1973)"},{"issue":"10","key":"1_CR69","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, 583 (1969)","journal-title":"Commun. ACM"},{"issue":"8","key":"1_CR70","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"1_CR71","volume-title":"The SPIN Model Checker","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Pearson Education, London (2003)"},{"key":"1_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509\u2013523. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_35"},{"issue":"1","key":"1_CR73","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1\u20139:67 (2016)","journal-title":"J. ACM"},{"issue":"1","key":"1_CR74","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016)","journal-title":"ACM Comput. Surv."},{"issue":"1\u20132","key":"1_CR75","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10994-013-5419-7","volume":"96","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1\u20132), 65\u201398 (2014)","journal-title":"Mach. Learn."},{"key":"1_CR76","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (August 2008)"},{"key":"1_CR77","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-17172-7_6","volume-title":"Verification, Induction, Termination Analysis","author":"M Johansson","year":"2010","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Dynamic rippling, middle-out reasoning and lemma discovery. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS (LNAI), vol. 6463, pp. 102\u2013116. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17172-7_6"},{"key":"1_CR78","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). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"1_CR79","doi-asserted-by":"crossref","unstructured":"Johnsen, E.B., Steffen, M., Stumpf, J.B.: Assumption-commitment types for resource management in virtually timed ambients. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 103\u2013121. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_6"},{"key":"1_CR80","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In; Mason, R.E.A. (ed.) Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, 19\u201323 September 1983, pp. 321\u2013332. North-Holland (1983)"},{"key":"1_CR81","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-030-29026-9_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"E Kamburjan","year":"2019","unstructured":"Kamburjan, E.: Behavioral program logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 391\u2013408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_22"},{"key":"1_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-98938-9_13","volume-title":"Integrated Formal Methods","author":"E Kamburjan","year":"2018","unstructured":"Kamburjan, E., Chen, T.-C.: Stateful behavioral types for active objects. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 214\u2013235. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_13"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Kamburjan, E.. Din, C.C., H\u00e4hnle, R., Johnsen, E.B.: Behavioral contracts for cooperative scheduling. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-030-64354-6_4"},{"key":"1_CR84","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/j.scico.2018.07.001","volume":"166","author":"E Kamburjan","year":"2018","unstructured":"Kamburjan, E., H\u00e4hnle, R., Sch\u00f6n, S.: Formal modeling and analysis of railway operations with Active Objects. Sci. Comput. Program. 166, 167\u2013193 (2018)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"1_CR85","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267\u2013288 (2011)","journal-title":"Formal Aspects Comput."},{"issue":"7","key":"1_CR86","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"1_CR87","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"1_CR88","doi-asserted-by":"crossref","unstructured":"Kn\u00fcppel, A., Runge, T., Schaefer, I.: Scaling correctness-by-construction. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020. LNCS, Rhodes, Greece, vol. 12476, pp. 187\u2013207. Springer, Heidelberg (October 2020)","DOI":"10.1007\/978-3-030-61362-4_10"},{"key":"1_CR89","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). https:\/\/doi.org\/10.1007\/978-3-642-27919-5"},{"key":"1_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"key":"1_CR91","unstructured":"Leavens, G.T., et al.: JML Reference Manual. Draft revision 2344 (May 2013)"},{"key":"1_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-87873-5_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"KRM Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P., Wallenburg, A.: Flexible immutability with frozen objects. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 192\u2013208. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87873-5_17"},{"key":"1_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/BFb0020971","volume-title":"Hybrid Systems III","author":"N Lynch","year":"1996","unstructured":"Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.B.: Hybrid I\/O automata. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 496\u2013510. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020971"},{"key":"1_CR94","unstructured":"McIlvenna, S., Dumas, M., Wynn, M.T.: Synthesis of orchestrators from service choreographies. In: Kirchberg, M., Link, S. (eds.) 6th Asia-Pacific Conference on Conceptual Modelling (APCCM), Conceptual Modelling 2009. CRPIT, Wellington, New Zealand, vol. 96, pp. 129\u2013138. Australian Computer Society (2009)"},{"issue":"10","key":"1_CR95","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"1_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"issue":"1","key":"1_CR97","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"I. Inf. Comput."},{"issue":"1","key":"1_CR98","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, II. Inf. Comput. 100(1), 41\u201377 (1992)","journal-title":"Inf. Comput."},{"issue":"4","key":"1_CR99","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"1_CR100","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/s10009-018-0502-9","volume":"20","author":"A M\u00fcller","year":"2018","unstructured":"M\u00fcller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Tactical contract composition for hybrid system component verification. Int. J. Softw. Tools Technol. Transf. 20(6), 615\u2013643 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"LP Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348\u2013362. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36575-3_24"},{"key":"1_CR102","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"2","key":"1_CR103","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3211968","volume":"62","author":"PW O\u2019Hearn","year":"2019","unstructured":"O\u2019Hearn, P.W.: Separation logic. Commun. ACM 62(2), 86\u201395 (2019)","journal-title":"Commun. ACM"},{"issue":"5","key":"1_CR104","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"issue":"10","key":"1_CR105","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/MC.2003.1236471","volume":"36","author":"C Peltz","year":"2003","unstructured":"Peltz, C.: Web services orchestration and choreography. IEEE Comput. 36(10), 46\u201352 (2003)","journal-title":"IEEE Comput."},{"key":"1_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11804192_15","volume-title":"Formal Methods for Components and Objects","author":"A Poetzsch-Heffter","year":"2006","unstructured":"Poetzsch-Heffter, A., Sch\u00e4fer, J.: Modular specification of encapsulated object-oriented components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 313\u2013341. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_15"},{"key":"1_CR107","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering: Foundations Principles and Techniques","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations Principles and Techniques. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/3-540-28901-1"},{"key":"1_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-57529-4_61","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"W Reif","year":"1993","unstructured":"Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 284\u2013293. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57529-4_61"},{"key":"1_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15579-6_6","volume-title":"Software Product Lines: Going Beyond","author":"I Schaefer","year":"2010","unstructured":"Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77\u201391. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15579-6_6"},{"issue":"4","key":"1_CR110","first-page":"377","volume":"3","author":"G Schellhorn","year":"1997","unstructured":"Schellhorn, G., Ahrendt, W.: Reasoning about abstract state machines: the WAM case study. J. Univ. Comput. Sci. 3(4), 377\u2013412 (1997)","journal-title":"J. Univ. Comput. Sci."},{"key":"1_CR111","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-18070-5_10","volume-title":"Formal Verification of Object-Oriented Software","author":"PH Schmitt","year":"2011","unstructured":"Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Dynamic frames in Java dynamic logic. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138\u2013152. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_10"},{"issue":"4","key":"1_CR112","first-page":"385","volume":"63","author":"M Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informatica 63(4), 385\u2013410 (2004)","journal-title":"Fundamenta Informatica"},{"key":"1_CR113","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science, London (1992)","edition":"2"},{"key":"1_CR114","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":"1_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-030-38808-9_8","volume-title":"Dynamic Logic. New Trends and Applications","author":"D Steinh\u00f6fel","year":"2020","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: The trace modality. In: Soares Barbosa, L., Baltag, A. (eds.) DALI 2019. LNCS, vol. 12005, pp. 124\u2013140. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-38808-9_8"},{"key":"1_CR116","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":"1_CR117","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Kuhlemann, M., Apel, S.: Proof composition for deductive verification of software product lines. In: 4th IEEE International Conference on Software Testing, Verification and Validation (Workshop Proceedings), ICST, Berlin, Germany, pp. 270\u2013277. IEEE Computer Society (2011)","DOI":"10.1109\/ICSTW.2011.48"},{"key":"1_CR118","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"},{"issue":"1\u20133","key":"1_CR119","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.tcs.2004.05.022","volume":"323","author":"P Urso","year":"2004","unstructured":"Urso, P., Kounalis, E.: Sound generalizations in mathematical induction. Theoret. Comput. Sci. 323(1\u20133), 443\u2013471 (2004)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"1_CR120","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0004-3702(99)00096-X","volume":"116","author":"C Walther","year":"2000","unstructured":"Walther, C., Kolbe, T.: Proving theorems by reuse. Artif. Intell. 116(1\u20132), 17\u201366 (2000)","journal-title":"Artif. Intell."},{"key":"1_CR121","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45085-6_28","volume-title":"Automated Deduction \u2013 CADE-19","author":"C Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About VeriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 322\u2013327. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_28"}],"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_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T04:40:38Z","timestamp":1669351238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_1"}},"subtitle":["Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification"],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":121,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_1","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"}}]}}