{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:01:10Z","timestamp":1742932870306,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544334"},{"type":"electronic","value":"9783662544341"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_31","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"831-854","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modular Verification of Higher-Order Functional Programs"],"prefix":"10.1007","author":[{"given":"Ryosuke","family":"Sato","sequence":"first","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-49213-5_4","volume-title":"Compositionality: The Significant Difference","author":"S Berezin","year":"1998","unstructured":"Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81\u2013102. Springer, Heidelberg (1998). doi:10.1007\/3-540-49213-5_4"},{"key":"31_CR2","unstructured":"Burch, J., Clarke, E.M., Long, D.: Symbolic model checking with partitioned transition relations. In: Proceedings of the IFIP TC10\/WG 10.5 International Conference on Very Large Scale Integration (VLSI 1991), pp. 49\u201358 (1991)"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Campos, S.V.A.: A quantitative approach to the formal verification of real-time systems. Ph.D. thesis, Carnegie Mellon University (1996)","DOI":"10.1007\/3-540-63166-6_46"},{"issue":"2","key":"31_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s11334-011-0148-1","volume":"7","author":"S Chaki","year":"2011","unstructured":"Chaki, S., Gurfinkel, A.: Automated assume-guarantee reasoning for omega-regular systems and specifications. Innov. Syst. Softw. Eng. 7(2), 131\u2013139 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0102s\u0102reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). doi:10.1007\/3-540-36577-X_24"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP 2013), pp. 125\u2013128 (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135\u2013148. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-70545-1_14"},{"issue":"3","key":"31_CR8","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp. 222\u2013233 (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 495\u2013508 (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"31_CR11","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). doi:10.1007\/978-3-642-17511-4_20"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-26529-2_16","volume-title":"Programming Languages and Systems","author":"Y Matsumoto","year":"2015","unstructured":"Matsumoto, Y., Kobayashi, N., Unno, H.: Automata-based abstraction for automated verification of higher-order tree-processing programs. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 295\u2013312. Springer, Cham (2015). doi:10.1007\/978-3-319-26529-2_16"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Nguyen, P.C., Horn, D.V.: Relatively complete counterexamples for higher-order programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 446\u2013456. ACM (2015)","DOI":"10.1145\/2737924.2737971"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Nguyen, P.C., Tobin-Hochstadt, S., Horn, D.V.: Soft contract verification. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014), pp. 139\u2013152 (2014)","DOI":"10.1145\/2628136.2628156"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pp. 587\u2013598 (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008), pp. 159\u2013169 (2008)","DOI":"10.1145\/1379022.1375602"},{"issue":"6","key":"31_CR17","first-page":"827","volume":"23","author":"R Sato","year":"2015","unstructured":"Sato, R., Asada, K., Kobayashi, N.: Refinement type checking via assertion checking. J. Inf. Process. 23(6), 827\u2013834 (2015)","journal-title":"J. Inf. Process."},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013), pp. 53\u201362. ACM Press (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Swamy, N., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S., Hri\u00c5\u00a3cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Swamy, N., Hri\u00c5\u00a3cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 256\u2013270 (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-47958-3_16","volume-title":"Programming Languages and Systems","author":"T Terao","year":"2016","unstructured":"Terao, T., Tsukada, T., Kobayashi, N.: Higher-order model checking in direct style. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 295\u2013313. Springer, Cham (2016). doi:10.1007\/978-3-319-47958-3_16"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 119\u2013130 (2010)","DOI":"10.1145\/1706299.1706315"},{"key":"31_CR22","unstructured":"Touati, H., Savoj, H., Lin, B., Brayton, R., Sangiovanni-Vincentelli, A.: Implicit state enumeration of finite state machines using BDD\u2019s. In: 1990 IEEE International Conference on Computer-Aided Design (ICCAD 1990), pp. 130\u2013133 (1990)"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp. 277\u2013288 (2009)","DOI":"10.1145\/1599410.1599445"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp. 75\u201386 (2013)","DOI":"10.1145\/2480359.2429081"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 269\u2013282 (2014)","DOI":"10.1145\/2628136.2628161"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Proceedings of the 6th ACM SIGPLAN Symposium on Scala (Scala 2015), pp. 18\u201329 (2015)","DOI":"10.1145\/2774975.2774978"},{"key":"31_CR27","unstructured":"Weis, P.: Caml examples (2001). http:\/\/caml.inria.fr\/pub\/old_caml_site\/Examples\/"},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1999), pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"},{"key":"31_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-35873-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Zhu","year":"2013","unstructured":"Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 295\u2013314. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35873-9_19"},{"key":"31_CR30","doi-asserted-by":"crossref","unstructured":"Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 400\u2013411 (2015)","DOI":"10.1145\/2784731.2784766"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI 2016), pp. 491\u2013507 (2016)","DOI":"10.1145\/2908080.2908125"}],"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-662-54434-1_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T15:58:39Z","timestamp":1635263919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}