{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:22:16Z","timestamp":1758979336881,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031510595"},{"type":"electronic","value":"9783031510601"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-51060-1_11","type":"book-chapter","created":{"date-parts":[[2024,1,28]],"date-time":"2024-01-28T07:02:08Z","timestamp":1706425328000},"page":"289-322","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Context-Aware Trace Contracts"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]},{"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Scaletta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,29]]},"reference":[{"key":"11_CR1","series-title":"LNCS","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, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"doi-asserted-by":"crossref","unstructured":"Albert, E., de la Banda, M.G., G\u00f3mez-Zamalloa, M., Isabel, M., Stuckey, P.J.: Optimal context-sensitive dynamic partial order reduction with observers. In: Zhang, D., M\u00f8ller, A. (eds.) Proceedings 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA, pp. 352\u2013362. ACM (2019)","key":"11_CR2","DOI":"10.1145\/3293882.3330565"},{"doi-asserted-by":"crossref","unstructured":"Aldrich, J., Sunshine, J., Saini, D., Sparks, Z.: Typestate-oriented programming. In: OOPSLA Companion, pp. 1015\u20131022. ACM (2009)","key":"11_CR3","DOI":"10.1145\/1639950.1640073"},{"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 7th Conference on Systems Software Verification. EPTCS, vol. 102, pp. 18\u201332 (2012)","key":"11_CR4","DOI":"10.4204\/EPTCS.102.4"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-38574-2_22","volume-title":"Automated Deduction \u2013 CADE-24","author":"B Beckert","year":"2013","unstructured":"Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 315\u2013329. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_22"},{"key":"11_CR6","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"},{"unstructured":"Bubel, R., Gurov, D., H\u00e4hnle, R., Scaletta, M.: Trace-based deductive verification. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Manizales Colombia. EPiC Series in Computing. EasyChair (2023)","key":"11_CR7"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"de Boer, F., et al.: A survey of active object languages. ACM Comput. Surv. 50(5), 76:1\u201376:39 (2017)","key":"11_CR9","DOI":"10.1145\/3122848"},{"issue":"1","key":"11_CR10","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. Reason. 62(1), 93\u2013126 (2019)","journal-title":"J. Autom. Reason."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465\u2013490. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_21"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517\u2013526. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35"},{"unstructured":"Din, C.C., H\u00e4hnle, R., Henrio, L., Johnsen, E.B., Pun, V.K.I., Tarifa, S.L.T.: LAGC semantics of concurrent programming languages. CoRR, abs\/2202.12195 (2022)","key":"11_CR13"},{"key":"11_CR14","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":"11_CR15","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."},{"key":"11_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"JV Guttag","year":"1993","unstructured":"Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4612-2704-5"},{"key":"11_CR17","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"},{"doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Kamburjan, E., Scaletta, M.: Context-aware trace contracts. CoRR, abs\/2310.04384 (2023)","key":"11_CR18","DOI":"10.1007\/978-3-031-51060-1_11"},{"key":"11_CR19","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":"4","key":"11_CR20","doi-asserted-by":"publisher","first-page":"935","DOI":"10.1145\/115234.115351","volume":"38","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935\u2013962 (1991)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Parikh, R.: Process logic: expressiveness, decidability, completeness. In: 21st Annual Symposium on Foundations of Computer Science, Syracuse, New York, USA, 13\u201315 October 1980, pp. 129\u2013142. IEEE Computer Society (1980)","key":"11_CR21","DOI":"10.1109\/SFCS.1980.35"},{"doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 273\u2013284 (2008)","key":"11_CR22","DOI":"10.1145\/1328438.1328472"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-49812-6_7","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"M Huisman","year":"2016","unstructured":"Huisman, M., Ahrendt, W., Grahl, D., Hentschel, M.: Formal specification with the java modeling language. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 193\u2013241. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_7"},{"key":"11_CR24","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"},{"unstructured":"Jones, C.B.: Developing methods for computer programs including a notion of interference. Ph.D. thesis, University of Oxford, UK (1981)","key":"11_CR25"},{"unstructured":"Jones, C.B.: Granularity and the development of concurrent programs. In: Brookes, S.D., Main, M.G., Melton, A., Mislove, M.W. (eds.) 11th Annual Conference on Mathematical Foundations of Programming Semantics, MFPS, New Orleans, LA, USA. ENTCS, vol. 1, pp. 302\u2013306. Elsevier (1995)","key":"11_CR26"},{"key":"11_CR27","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":"11_CR28","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":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-47846-3_19","volume-title":"Formal Methods and Software Engineering","author":"E Kamburjan","year":"2016","unstructured":"Kamburjan, E., Din, C.C., Chen, T.-C.: Session-based compositional analysis for actor-based languages using futures. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 296\u2013312. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_19"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-64354-6_4","volume-title":"Deductive Software Verification: Future Perspectives","author":"E Kamburjan","year":"2020","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, pp. 85\u2013121. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_4"},{"key":"11_CR31","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.102928","volume":"226","author":"E Kamburjan","year":"2023","unstructured":"Kamburjan, E., Scaletta, M., Rollshausen, N.: Deductive verification of active objects with crowbar. Sci. Comput. Program. 226, 102928 (2023)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"11_CR32","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. Form. Asp. Comput. 23(3), 267\u2013288 (2011)","journal-title":"Form. Asp. Comput."},{"unstructured":"Leavens, G.T., et al.: JML Reference Manual (2013). Draft revision 2344","key":"11_CR33"},{"issue":"6","key":"11_CR34","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"10","key":"11_CR35","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\u2019\u2019. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"unstructured":"Mota, J., Giunti, M., Ravara, A.: On using verifast, vercors, plural, and key to check object usage. CoRR, abs\/2209.05136 (2022)","key":"11_CR36"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"issue":"1","key":"11_CR38","first-page":"1","volume":"11","author":"K Nakata","year":"2015","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1), 1\u201332 (2015)","journal-title":"Log. Methods Comput. Sci."},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"PW O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49\u201367. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pp. 46\u201357. IEEE Computer Society (1977)","key":"11_CR40","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","key":"11_CR41","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR42","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56, 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Lecture Notes in Computer Science","Active Object Languages: Current Research Trends"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-51060-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,9]],"date-time":"2024-11-09T10:08:21Z","timestamp":1731146901000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-51060-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031510595","9783031510601"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-51060-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 January 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}