{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:18:24Z","timestamp":1783009104313,"version":"3.54.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319737201","type":"print"},{"value":"9783319737218","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_2","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"25-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Gradual Program Verification"],"prefix":"10.1007","author":[{"given":"Johannes","family":"Bader","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-06200-6_27","volume-title":"NASA Formal Methods","author":"S Arlt","year":"2014","unstructured":"Arlt, S., Rubio-Gonz\u00e1lez, C., R\u00fcmmer, P., Sch\u00e4f, M., Shankar, N.: The gradual verifier. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 313\u2013327. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_27"},{"issue":"3","key":"2_CR2","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of jml tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212\u2013232 (2005). http:\/\/dx.doi.org\/10.1007\/s10009-004-0167-4","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2_CR3","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the java modeling language (jml) (2002)"},{"issue":"8","key":"2_CR4","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). http:\/\/doi.acm.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Fahndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: ACM SAC - OOPS. Association for Computing Machinery, Inc., March 2010. https:\/\/www.microsoft.com\/en-us\/research\/publication\/embedded-contract-languages\/","DOI":"10.1145\/1774088.1774531"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of the 7th ACM SIGPLAN Conference on Functional Programming (ICFP 2002), Pittsburgh, PA, USA, pp. 48\u201359, September 2002","DOI":"10.1145\/581478.581484"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Garcia, R., Clark, A.M., Tanter, E.: Abstracting gradual typing. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 429\u2013442. ACM, New York (2016). http:\/\/doi.acm.org\/10.1145\/2837614.2837670","DOI":"10.1145\/2837614.2837670"},{"issue":"10","key":"2_CR8","doi-asserted-by":"crossref","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. Communications of the ACM 12(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Lehmann, N., Tanter, \u00c9.: Gradual refinement types. In: Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017), Paris, France, pp. 775\u2013788, January 2017","DOI":"10.1145\/3009837.3009856"},{"key":"2_CR10","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":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., 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"},{"issue":"3","key":"2_CR11","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0164-1212(88)90022-2","volume":"8","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Eiffel: A language and environment for software engineering. Journal of Systems and Software 8(3), 199\u2013246 (1988)","journal-title":"Journal of Systems and Software"},{"key":"2_CR12","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall (1988)"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"5\u20136","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisset, G., Birkedal, L.: Hoare type theory, polymorphism and separation. Journal of Functional Programming 5\u20136, 865\u2013911 (2008)","journal-title":"Journal of Functional Programming"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-78163-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"HH Nguyen","year":"2008","unstructured":"Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime checking for separation logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 203\u2013217. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_19"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science 2002, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-642-28869-2_29","volume-title":"Programming Languages and Systems","author":"I Sergey","year":"2012","unstructured":"Sergey, I., Clarke, D.: Gradual ownership types. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 579\u2013599. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_29"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73589-2_2","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"J Siek","year":"2007","unstructured":"Siek, J., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2\u201327. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73589-2_2"},{"key":"2_CR18","unstructured":"Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming Workshop, vol. 6, pp. 81\u201392 (2006)"},{"key":"2_CR19","unstructured":"Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T.: Refined criteria for gradual typing. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"J Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148\u2013172. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03013-0_8"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-22655-7_22","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"R Wolff","year":"2011","unstructured":"Wolff, R., Garcia, R., Tanter, \u00c9., Aldrich, J.: Gradual typestate. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 459\u2013483. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22655-7_22"},{"issue":"1","key":"2_CR22","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A Wright","year":"1994","unstructured":"Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994). http:\/\/dx.doi.org\/10.1006\/inco.1994.1093","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T16:00:35Z","timestamp":1570550435000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}