{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:29Z","timestamp":1790927609953,"version":"4.1.0"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning.  \u2019s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and thread-modular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers,  restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the  language and describe key aspects of the supported proof automation. We evaluate  on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that  improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris\/Rocq proof mode.<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_4","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T09:15:20Z","timestamp":1753175720000},"page":"81-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Raven: An SMT-Based Concurrency Verifier"],"prefix":"10.1007","author":[{"given":"Ekanshdeep","family":"Gupta","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nisarg","family":"Patel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-65630-9_1","volume-title":"Computer Aided Verification, CAV 2024, Part II","author":"L Armborst","year":"2024","unstructured":"Armborst, L., et al.: The vercors verifier: a progress report. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024, Part II. LNCS, vol. 14682, pp. 3\u201318. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-031-06773-0_5","volume-title":"NASA Formal Methods, NFM 2022","author":"V Astrauskas","year":"2022","unstructured":"Astrauskas, V., et al.: The Prusti project: formal verification for rust. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 88\u2013108. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"B\u00edl\u00fd, A., Pereira, J.C., Sch\u00e4r, J., M\u00fcller, P.: Refinement proofs in Rust using ghost locks. CoRR abs\/2311.14452 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.14452","DOI":"10.48550\/ARXIV.2311.14452"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Bizjak, A., Gratzer, D., Krebbers, R., Birkedal, L.: Iron: Managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3(POPL), 65:1\u201365:30 (2019). https:\/\/doi.org\/10.1145\/3290378","DOI":"10.1145\/3290378"},{"key":"4_CR6","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.) Integrated Formal Methods, pp. 102\u2013110. Springer, Cham (2017)"},{"key":"4_CR7","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-031-13188-2_7","volume-title":"Computer Aided Verification - CAV 2022, Part II","author":"T Dardinier","year":"2022","unstructured":"Dardinier, T., Parthasarathy, G., Weeks, N., M\u00fcller, P., Summers, A.J.: Sound automation of magic wands. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part II. LNCS, vol. 13372, pp. 130\u2013151. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_7"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Dardinier, T., Sammler, M., Parthasarathy, G., Summers, A.J., M\u00fcller, P.: Formal foundations for translational separation logic verifiers. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704856","DOI":"10.1145\/3704856"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - 23\u201325 January 2013, pp. 287\u2013300. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"T Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper - automatic verification for fine-grained concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420\u2013447. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_16"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Fromherz, A., et al.: Steel: proof-oriented programming in a dependently typed concurrent separation logic. Proc. ACM Program. Lang. 5(ICFP), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3473590","DOI":"10.1145\/3473590"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"G\u00e4her, L., Sammler, M., Jung, R., Krebbers, R., Dreyer, D.: RefinedRust: a type system for high-assurance verification of Rust programs. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656422","DOI":"10.1145\/3656422"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Gupta, E., Nisarg, P., Wies, T.: Raven: an SMT-based concurrency verifier (2025). https:\/\/doi.org\/10.5281\/zenodo.15477369","DOI":"10.5281\/zenodo.15477369"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 271\u2013282. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926417","DOI":"10.1145\/1926385.1926417"},{"key":"4_CR18","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_CR19","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2(POPL), 1\u201334 (2017)","DOI":"10.1145\/3158154"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Jung, R., et al.: The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4(POPL), 45:1\u201345:32 (2020). https:\/\/doi.org\/10.1145\/3371113","DOI":"10.1145\/3371113"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 637\u2013650. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. J. Autom. Reason. 9(2), 261\u2013288 (1992). https:\/\/doi.org\/10.1007\/BF00245463","DOI":"10.1007\/BF00245463"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-27705-4_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"IT Kassios","year":"2012","unstructured":"Kassios, I.T., M\u00fcller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 196\u2013208. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_16"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Kragl, B., Qadeer, S.: The Civl verifier. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19\u201322 October 2021, pp. 143\u2013152. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_23, https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_23","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_23"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Krebbers, R., et al.: Mosel: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2(ICFP), 77:1\u201377:30 (2018). https:\/\/doi.org\/10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Krishna, S., Patel, N., Shasha, D.E., Wies, T.: Verifying concurrent search structure templates. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 181\u2013196. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386029","DOI":"10.1145\/3385412.3386029"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Krishna, S., Shasha, D.E., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang. 2(POPL), 37:1\u201337:31 (2018). https:\/\/doi.org\/10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-030-44914-8_12","volume-title":"Programming Languages and Systems","author":"S Krishna","year":"2020","unstructured":"Krishna, S., Summers, A.J., Wies, T.: Local reasoning for global graph properties. In: ESOP 2020. LNCS, vol. 12075, pp. 308\u2013335. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_12"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Qadeer, S., Walker, D.: Linear maps. In: Jhala, R., Swierstra, W. (eds.) Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, 29 January 2011, pp. 3\u201314. ACM (2011). https:\/\/doi.org\/10.1145\/1929529.1929531","DOI":"10.1145\/1929529.1929531"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"K Leino","year":"2009","unstructured":"Leino, K., M\u00fcller, P., Smans, J.: Verification of concurrent programs with chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_7"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Mansky, W., Du, K.: An Iris instance for verifying CompCert C programs, 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632848","DOI":"10.1145\/3632848"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Mulder, I., Krebbers, R.: Proof automation for linearizability in separation logic. Proc. ACM Program. Lang. 7(OOPSLA1), 462\u2013491 (2023). https:\/\/doi.org\/10.1145\/3586043","DOI":"10.1145\/3586043"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Mulder, I., Krebbers, R., Geuvers, H.: Diaframe: automated verification of fine-grained concurrent programs in Iris. In: Jhala, R., Dillig, I. (eds.) PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13\u201317 June 2022, pp. 809\u2013824. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523432","DOI":"10.1145\/3519939.3523432"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-41528-4_22","volume-title":"Computer Aided Verification","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part I. LNCS, vol. 9779, pp. 405\u2013425. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_22"},{"key":"4_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. (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_CR38","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Banerjee, A., Delbianco, G.A., F\u00e1bregas, I.: Specifying concurrent programs in separation logic: morphisms and simulations. Proc. ACM Program. Lang. 3(OOPSLA), 161:1\u2013161:30 (2019). https:\/\/doi.org\/10.1145\/3360587","DOI":"10.1145\/3360587"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/978-3-030-81688-9_33","volume-title":"Computer Aided Verification","author":"G Parthasarathy","year":"2021","unstructured":"Parthasarathy, G., M\u00fcller, P., Summers, A.J.: Formally validating a practical verification condition generator. In: Silva, A., Leino, K. (eds.) CAV 2021, Part II. LNCS, vol. 12760, pp. 704\u2013727. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773\u2013789. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_54"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_47"},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-54862-8_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124\u2013139. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_9"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P da Rocha Pinto","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"4_CR44","unstructured":"Schwerhoff, M.: Voila GitHub issue #33. https:\/\/github.com\/viperproject\/voila\/issues\/33. Accessed 15 Apr 2025"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1\u20132:58 (2012). https:\/\/doi.org\/10.1145\/2160910.2160911","DOI":"10.1145\/2160910.2160911"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 256\u2013270. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Swamy, N., Rastogi, A., Fromherz, A., Merigoux, D., Ahman, D., Mart\u00ednez, G.: SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. Proc. ACM Program. Lang. 4(ICFP), 121:1\u2013121:30 (2020). https:\/\/doi.org\/10.1145\/3409003","DOI":"10.1145\/3409003"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-319-63387-9_27","volume-title":"Computer Aided Verification","author":"M Windsor","year":"2017","unstructured":"Windsor, M., Dodds, M., Simner, B., Parkinson, M.J.: Starling: lightweight concurrency verification with views. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part I. LNCS, vol. 10426, pp. 544\u2013569. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_27"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Wolf, F.A., Schwerhoff, M., M\u00fcller, P.: Concise outlines for a complex logic: a proof outline checker for tada. Formal Methods Syst. Des. 61(1), 110\u2013136 (2022) https:\/\/doi.org\/10.1007\/s10703-023-00427-w","DOI":"10.1007\/s10703-023-00427-w"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98668-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:13:36Z","timestamp":1777302816000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}