{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T04:14:30Z","timestamp":1746591270125,"version":"3.40.5"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911200"},{"type":"electronic","value":"9783031911217"}],"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,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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> We introduce <jats:sc>coma<\/jats:sc>, a formally defined intermediate verification language. Specification annotations in <jats:sc>coma<\/jats:sc> take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the \u201cinterface\u201d part of the code, which is verified at every call site, from the \u201cimplementation\u201d part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths.<\/jats:p>\n          <jats:p>We define a verification condition generator for <jats:sc>coma<\/jats:sc> and prove its correctness. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In addition, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of <jats:sc>coma<\/jats:sc> on two non-trivial examples, which have been formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_8","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:22:39Z","timestamp":1746184959000},"page":"175-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["coma, an Intermediate Verification Language with Explicit Abstraction Barriers"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Paskevich","sequence":"first","affiliation":[]},{"given":"Paul","family":"Patault","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/s001650050041","volume":"11","author":"P Audebaud","year":"1999","unstructured":"Audebaud, P., Zucca, E.: Deriving proof rules from continuation semantics. Formal aspects of computing 11, 426\u2013447 (1999)","journal-title":"Formal aspects of computing"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP). vol. 46(9), pp. 418\u2013430. ACM, Tokyo, Japan (September 2011)","DOI":"10.1145\/2034773.2034828"},{"key":"8_CR3","unstructured":"Conchon, S., Coquereau, A., Iguernelala, M., Mebsout, A.: Alt-Ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)"},{"key":"8_CR4","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\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. vol.\u00a04963, pp. 337\u2013340. Springer (2008)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Denis, X., Jourdan, J.-H., March\u00e9, C.: Creusot: a foundry for the deductive verification of Rust programs. In: International Conference on Formal Engineering Methods. vol. 13478, pp. 90\u2013105. Springer (2022)","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming. Lecture Notes in Computer Science, vol.\u00a07792, pp. 125\u2013128. Springer (Mar 2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Principles Of Programming Languages. vol. 36(3), pp. 193\u2013205. ACM (2001)","DOI":"10.1145\/373243.360220"},{"key":"8_CR8","unstructured":"Fung, S.P.Y.: Is this the simplest (and most surprising) sorting algorithm ever? arXiv preprint arXiv:2110.01111 (2021)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Connection between Dijkstra\u2019s predicate-transformers and denotational continuation-semantics. DAIMI Report Series 86 (1978)","DOI":"10.7146\/dpb.v7i86.6502"},{"key":"8_CR10","unstructured":"Krivine, J.-L.: Un interpr\u00e8teur du $$\\lambda $$-calcul. Unpublished report (1985)"},{"key":"8_CR11","unstructured":"Kura, S.: Higher-Order Weakest Precondition Transformers via a CPS transformation. arXiv preprint arXiv:2301.09997 (2023)"},{"issue":"6","key":"8_CR12","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters 93(6), 281\u2013288 (2005)","journal-title":"Information Processing Letters"},{"key":"8_CR13","unstructured":"Leino, K.R.M.: This is Boogie 2. KRML Manuscript 178 (2008)"},{"key":"8_CR14","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: Verification, Model Checking, and Abstract Interpretation: 17th International Conference. vol.\u00a09583, pp. 41\u201362. Springer (2016)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Paskevich, A., Patault, P., Filli\u00e2tre, J.-C.: Coma, an Intermediate Verification Language with Explicit Abstraction Barriers (extended version). Tech. rep. (2025), https:\/\/hal.science\/hal-04839768","DOI":"10.1007\/978-3-031-91121-7_8"},{"issue":"2\u20133","key":"8_CR16","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R Statman","year":"1985","unstructured":"Statman, R.: Logical relations and the typed $$\\lambda $$-calculus. Information and control 65(2-3), 85\u201397 (1985)","journal-title":"Information and control"},{"issue":"6","key":"8_CR17","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/2499370.2491978","volume":"48","author":"N Swamy","year":"2013","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. ACM SIGPLAN Notices 48(6), 387\u2013398 (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1020887011500","volume":"15","author":"H Thielecke","year":"2002","unstructured":"Thielecke, H.: Comparing control constructs by double-barrelled CPS. Higher-Order and Symbolic Computation 15, 141\u2013160 (2002)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:32:56Z","timestamp":1746520376000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}