{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:10:21Z","timestamp":1755839421672,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031198489"},{"type":"electronic","value":"9783031198496"}],"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-19849-6_4","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"45-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Hoare Logic with\u00a0Regular Behavioral Specifications"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Knapp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Almeida, R., Broda, S., Moreira, N.: Deciding KAT and Hoare logic with derivatives. arXiv preprint arXiv:1210.2456 (2012)","DOI":"10.4204\/EPTCS.96.10"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-11319-2_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Alur","year":"2010","unstructured":"Alur, R., Chaudhuri, S.: Temporal reasoning for procedural programs. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 45\u201360. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11319-2_7"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-Based Verification of Functional Behaviour of Concurrent Programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84\u201398. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_6","DOI":"10.1007\/978-3-319-22969-0_6"},{"issue":"1\u20134","key":"4_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/176454.176487","volume":"2","author":"P Bumbulis","year":"1993","unstructured":"Bumbulis, P., Cowan, D.D.: RE2C: a more versatile scanner generator. ACM Lett. Program. Lang. Syst. (LOPLAS) 2(1\u20134), 70\u201384 (1993)","journal-title":"ACM Lett. Program. Lang. Syst. (LOPLAS)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 57\u201368 (2002)","DOI":"10.1145\/543552.512538"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/503271.503226","volume":"26","author":"L De Alfaro","year":"2001","unstructured":"De Alfaro, L., Henzinger, T.A.: Interface automata. ACM SIGSOFT Softw. Eng. Notes 26(5), 109\u2013120 (2001)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Disney, T., Flanagan, C., McCarthy, J.: Temporal higher-order contracts. In: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, pp. 176\u2013188 (2011)","DOI":"10.1145\/2034773.2034800"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-94583-1_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Ernst","year":"2022","unstructured":"Ernst, G.: Loop verification with invariants and contracts. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 69\u201392. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_4"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-030-25543-5_13","volume-title":"Computer Aided Verification","author":"G Ernst","year":"2019","unstructured":"Ernst, G., Murray, T.: SecCSL: Security Concurrent Separation Logic. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 208\u2013230. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_13"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-69149-5_41","volume-title":"Verified Software: Theories, Tools, Experiments","author":"ECR Hehner","year":"2008","unstructured":"Hehner, E.C.R.: Specified Blocks. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 384\u2013391. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_41"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"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. (CSUR) 49(1), 1\u201336 (2016)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-030-61362-4_29","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B Jacobs","year":"2020","unstructured":"Jacobs, B.: Modular verification of liveness properties of the I\/O behavior of imperative programs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 509\u2013524. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_29"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"4_CR16","unstructured":"Jacobs, B., Smans, J., Piessens, F.: VeriFast: Imperative programs as proofs. In: VSTTE workshop on Tools & Experiments (2010)"},{"issue":"3","key":"4_CR17","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. (TOPLAS) 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C Morgan","year":"1988","unstructured":"Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. (TOPLAS) 10(3), 403\u2013419 (1988)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"4_CR20","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"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics","author":"K Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for while. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 375\u2013390. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_26"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. In: Proceedings of the ACM on Programming Languages 4(POPL), 1\u201332 (2019)","DOI":"10.1145\/3371078"},{"issue":"11","key":"4_CR23","doi-asserted-by":"publisher","first-page":"3928","DOI":"10.3390\/app10113928","volume":"10","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Gurov, D., Huisman, M.: An abstraction technique for verifying shared-memory concurrency. Appl. Sci. 10(11), 3928 (2020)","journal-title":"Appl. Sci."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Penninckx, W., Timany, A., Jacobs, B.: Specifying I\/O using abstract nested Hoare triples in separation logic. In: Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, pp. 1\u20137 (2019)","DOI":"10.1145\/3340672.3341118"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: Safety verification of smart contracts. In: 2020 IEEE symposium on security and privacy (SP), pp. 1661\u20131677, IEEE (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46\u201357, ieee (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR27","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of Logic in Computer Science (LICS), pp. 55\u201374, IEEE (2002)"},{"issue":"1","key":"4_CR28","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s10472-013-9389-z","volume":"71","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: Rgitl: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71(1), 131\u2013174 (2014)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10270-013-0321-0","volume":"14","author":"S Soleimanifard","year":"2013","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: Procedure-modular specification and verification of temporal safety properties. Softw. Syst. Modeling 14(1), 83\u2013100 (2013). https:\/\/doi.org\/10.1007\/s10270-013-0321-0","journal-title":"Softw. Syst. Modeling"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Sprenger, C., et al.: Igloo: Soundly linking compositional refinement and separation logic for distributed system verification. In: Proceedings of the ACM on Programming Languages 4(OOPSLA), 1\u201331 (2020)","DOI":"10.1145\/3428220"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: A decade of dependent session types. In: 23rd International Symposium on Principles and Practice of Declarative Programming, pp. 1\u20133 (2021)","DOI":"10.1145\/3479394.3479398"},{"key":"4_CR32","unstructured":"Tuerk, T.: Local reasoning about while-loops. Proc. of Verified Software: Theory, Tools, and Experiments (VSTTE) 2010, 29 (2010)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-99725-4_24","volume-title":"Static Analysis","author":"C Urban","year":"2018","unstructured":"Urban, C., Ueltschi, S., M\u00fcller, P.: Abstract interpretation of CTL properties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 402\u2013422. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_24"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Uustalu, T., Nakata, K.: A hoare logic for the coinductive trace-based big-step semantics of while. Logical Methods Comput. Sci. 11(1), 488\u2013506 (2015)","DOI":"10.2168\/LMCS-11(1:1)2015"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:05:54Z","timestamp":1666224354000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_4","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":"17 October 2022","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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}