{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:34:17Z","timestamp":1742942057487,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081651"},{"type":"electronic","value":"9783031081668"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_11","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"229-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Alice in\u00a0Wineland: A Fairy Tale with\u00a0Contracts"],"prefix":"10.1007","author":[{"given":"Dilian","family":"Gurov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Lidstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"issue":"1\u20132","key":"11_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2008.09.004","volume":"74","author":"I Aktug","year":"2008","unstructured":"Aktug, I., Naliuka, K.: ConSpec - a formal language for policy specification. Sci. Comput. Program. 74(1\u20132), 2\u201312 (2008). https:\/\/doi.org\/10.1016\/j.scico.2008.09.004","journal-title":"Sci. Comput. Program."},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of ACM Symposium on Theory of Computing (STOC 2004), pp. 202\u2013211. Association for Computing Machinery (2004). https:\/\/doi.org\/10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495\u2013499. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_44"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"11_CR6","unstructured":"Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Interval temporal logics: a journey. Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 3(105), 81\u2013107 (2011)"},{"issue":"3","key":"11_CR7","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987). https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"11_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"11_CR9","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2007","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Pearson international edition, Addison-Wesley, Boston (2007)","edition":"3"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR11","unstructured":"Leavens, G.T., et al.: JML reference manual (2008)"},{"issue":"10","key":"11_CR12","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). https:\/\/doi.org\/10.1109\/2.161279","journal-title":"IEEE Comput."},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A hoare logic for the coinductive trace-based big-step semantics of while. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488\u2013506. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_26"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-39322-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Gurov, D., Huisman, M.: Practical abstractions for automated verification of shared-memory concurrency. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 401\u2013425. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_19"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.ic.2015.11.009","volume":"246","author":"J Rot","year":"2016","unstructured":"Rot, J., Bonsangue, M., Rutten, J.: Proving language inclusion and equivalence by coinduction. Inf. Comput. 246, 62\u201376 (2016). https:\/\/doi.org\/10.1016\/j.ic.2015.11.009","journal-title":"Inf. Comput."},{"key":"11_CR17","unstructured":"Wing, J.M.: A Two-Tiered Approach to Specifying Programs. Ph.D. thesis, Technical Report TR-299 (1983)"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:39:48Z","timestamp":1656891588000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}