{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:32:01Z","timestamp":1777890721370,"version":"3.51.4"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_21","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"589-618","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Program Verification by Coinduction"],"prefix":"10.1007","author":[{"given":"Brandon","family":"Moore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigore","family":"Rosu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"10","key":"21_CR1","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). \nhttps:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"issue":"6","key":"21_CR2","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1145\/2813885.2737979","volume":"50","author":"Chris Hathhorn","year":"2015","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: PLDI, pp. 336\u2013345. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2737924.2737979","journal-title":"ACM SIGPLAN Notices"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Bogd\u0103na\u015f, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. In: POPL, pp. 445\u2013456. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Bodin, M., Chargueraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: POPL, pp. 87\u2013100. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"issue":"6","key":"21_CR5","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/2813885.2737991","volume":"50","author":"Daejun Park","year":"2015","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of Javascript. In: PLDI, pp. 346\u2013356. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2737924.2737991","journal-title":"ACM SIGPLAN Notices"},{"issue":"10","key":"21_CR6","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/2544173.2509536","volume":"48","author":"Joe Gibbs Politz","year":"2013","unstructured":"Politz, J.G., Martinez, A., Milano, M., Warren, S., Patterson, D., Li, J., Chitipothu, A., Krishnamurthi, S.: Python: the full monty. In: OOPSLA, pp. 217\u2013232. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2509136.2509536","journal-title":"ACM SIGPLAN Notices"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-662-44202-9_23","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"D Filaretti","year":"2014","unstructured":"Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 567\u2013592. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-44202-9_23"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78739-6_1","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2008","unstructured":"Owens, S.: A sound semantics for OCaml$$_{light}$$light. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1\u201315. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78739-6_1"},{"issue":"6","key":"21_CR9","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. LAP 79(6), 397\u2013434 (2010). \nhttps:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","journal-title":"J. LAP"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: POPL, pp. 285\u2013296. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2103656.2103691","DOI":"10.1145\/2103656.2103691"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: effective tool support for the working semanticist. In: ICFP. ACM (2007). \nhttps:\/\/doi.org\/10.1017\/S0956796809990293","DOI":"10.1017\/S0956796809990293"},{"issue":"3","key":"21_CR12","first-page":"366","volume":"8","author":"T Uustalu","year":"2001","unstructured":"Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nord. J. Comput. 8(3), 366\u2013390 (2001)","journal-title":"Nord. J. Comput."},{"key":"21_CR13","unstructured":"Bartels, F.: On generalised coinduction and probabilistic specification formats: distributive laws in coalgebraic modelling. Ph.D. thesis, Vrije Universiteit Amsterdam (2004)"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Pous, D.: Coinduction all the way up. In: LICS, pp. 307\u2013316. IEEE (2016). \nhttps:\/\/doi.org\/10.1145\/2933575.2934564","DOI":"10.1145\/2933575.2934564"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"\u015etef\u0103nescu, A., Park, D., Yuwen, S., Li, Y., Ro\u015fu, G.: Semantics-based program verifiers for all languages. In: OOPSLA, pp. 74\u201391. ACM (2016). \nhttps:\/\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"21_CR16","unstructured":"Moore, B., Pe\u00f1a, L., Rosu, G.: GitHub repository (2017). \nhttps:\/\/github.com\/Formal-Systems-Laboratory\/coinduction\n\n. Source code"},{"issue":"1","key":"21_CR17","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1992","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1992). \nhttps:\/\/doi.org\/10.1006\/inco.1994.1093","journal-title":"Inf. Comput."},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.05.001","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Program. 60\u201361, 17\u2013139 (2004). \nhttps:\/\/doi.org\/10.1016\/j.jlap.2004.05.001","journal-title":"J. Log. Algebraic Program."},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE (2002). \nhttps:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"2","key":"21_CR20","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symbolic Log. 5(2), 215\u2013244 (1999). \nhttps:\/\/doi.org\/10.2307\/421090","journal-title":"Bull. Symbolic Log."},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Felleisen, M., Friedman, D.P.: A calculus for assignments in higher-order languages. In: POPL, p. 314. ACM (1987). \nhttps:\/\/doi.org\/10.1145\/41625.41654","DOI":"10.1145\/41625.41654"},{"key":"21_CR22","unstructured":"Felleisen, M.: The calculi of Lambda-$$\\nu $$\u03bd-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph.D. thesis, Indiana University (1987)"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G.: Matching logic \u2013 extended abstract. In: RTA, LIPIcs, pp. 5\u201321. Schloss Dagstuhl-LZ I (2015). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.5","DOI":"10.4230\/LIPIcs.RTA.2015.5"},{"issue":"6","key":"21_CR24","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/1993316.1993526","volume":"46","author":"Adam Chlipala","year":"2011","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234\u2013245. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1993498.1993526","journal-title":"ACM SIGPLAN Notices"},{"issue":"8","key":"21_CR25","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H Schorr","year":"1967","unstructured":"Schorr, H., Waite, W.M.: An efficient machine-independent procedure for garbage collection in various list structures. Commun. ACM 10(8), 501\u2013506 (1967). \nhttps:\/\/doi.org\/10.1145\/363534.363554","journal-title":"Commun. ACM"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102\u2013126. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722010_8"},{"issue":"1\u20132","key":"21_CR27","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1\u20132), 200\u2013227 (2005). \nhttps:\/\/doi.org\/10.1016\/j.ic.2004.10.007","journal-title":"Inf. Comput."},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Hubert, T., Marche, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: SEFM, pp. 190\u2013199. IEEE (2005). \nhttps:\/\/doi.org\/10.1109\/SEFM.2005.1","DOI":"10.1109\/SEFM.2005.1"},{"issue":"3","key":"21_CR29","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00289068","volume":"11","author":"D Gries","year":"1979","unstructured":"Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informatica 11(3), 223\u2013232 (1979). \nhttps:\/\/doi.org\/10.1007\/BF00289068","journal-title":"Acta Informatica"},{"issue":"1","key":"21_CR30","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/1328897.1328459","volume":"43","author":"Ashutosh Gupta","year":"2008","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: POPL, pp. 147\u2013158. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1328438.1328459","journal-title":"ACM SIGPLAN Notices"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-Y Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156\u2013171. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_11"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: ICFP, pp. 391\u2013402. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2500365.2500592","DOI":"10.1145\/2500365.2500592"},{"key":"21_CR33","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Moore, B.M.: One-path reachability logic. In: LICS, pp. 358\u2013367. IEEE (2013). \nhttps:\/\/doi.org\/10.1109\/LICS.2013.42","DOI":"10.1109\/LICS.2013.42"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-32759-9_32","volume-title":"FM 2012: Formal Methods","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: From Hoare logic to matching logic reachability. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 387\u2013402. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_32"},{"key":"21_CR35","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A., Ciob\u00e2c\u0103, c., Moore, B.M.: Reachability logic. Technical report, University of Illinois, July 2012. \nhttp:\/\/hdl.handle.net\/2142\/32952"},{"key":"21_CR36","doi-asserted-by":"publisher","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637\u2013650. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2775051.2676980","DOI":"10.1145\/2775051.2676980"},{"key":"21_CR37","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\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"21_CR38","unstructured":"Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research, June 2008"},{"key":"21_CR39","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"Mike Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: 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). \nhttps:\/\/doi.org\/10.1007\/11804192_17"},{"key":"21_CR40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, New York (2014)"},{"key":"21_CR41","doi-asserted-by":"publisher","unstructured":"Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: ICFP, pp. 175\u2013188. ACM (2004). \nhttps:\/\/doi.org\/10.1145\/1016850.1016875","DOI":"10.1145\/1016850.1016875"},{"key":"21_CR42","doi-asserted-by":"publisher","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: PLDI, pp. 401\u2013414. ACM (2006). \nhttps:\/\/doi.org\/10.1145\/1133981.1134028","DOI":"10.1145\/1133981.1134028"},{"key":"21_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-87873-5_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"X Feng","year":"2008","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 54\u201369. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-87873-5_8"},{"issue":"1","key":"21_CR44","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/2480359.2429093","volume":"48","author":"Chung-Kil Hur","year":"2013","unstructured":"Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL, pp. 193\u2013206. ACM (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"21_CR45","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:13:39Z","timestamp":1523654019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}