{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:32:49Z","timestamp":1725867169272},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47958-3_16","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T13:40:52Z","timestamp":1475934052000},"page":"295-313","source":"Crossref","is-referenced-by-count":2,"title":["Higher-Order Model Checking in Direct Style"],"prefix":"10.1007","author":[{"given":"Taku","family":"Terao","sequence":"first","affiliation":[]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1\u201320. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24756-2_1"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of PASTE 2001, pp. 97\u2013103. ACM (2001)","DOI":"10.1145\/379605.379690"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Broadbent, C.H., Carayol, A., Hague, M., Serre, O.: C-SHORe: acollapsible approach to higher-order verification. In: Proceedings of ICFP 2013, pp. 13\u201324 (2013)","DOI":"10.1145\/2500365.2500589"},{"key":"16_CR4","unstructured":"Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013, LIPIcs, vol. 23, pp. 129\u2013148 (2013)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Gilray, T., Lyde, S., Adams, M.D., Might, M., Horn, D.V.: Pushdown control-flow analysis for free. In: Proceedings of POPL 2016, pp. 691\u2013704. ACM (2016)","DOI":"10.1145\/2837614.2837631"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Horn, D.V., Might, M.: Abstracting abstract machines. In: Proceedings of ICFP 2010, pp. 51\u201362. ACM (2010)","DOI":"10.1145\/1863543.1863553"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Johnson, J.I., Horn, D.V.: Abstracting abstract control. In: Proceedings of DLS 2014, pp. 11\u201322. ACM (2014)","DOI":"10.1145\/2775052.2661098"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25\u201336. ACM (2009)","DOI":"10.1145\/1599410.1599415"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3) (2013)","DOI":"10.1145\/2487241.2487246"},{"key":"16_CR10","unstructured":"Kobayashi, N.: HorSat2: a saturation-based higher-order model checker. A toolpaper under submission (2015). http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~koba\/horsat2"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI 2011, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993498.1993525"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-54833-8_21","volume-title":"Programming Languages and Systems","author":"T Kuwahara","year":"2014","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 392\u2013411. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54833-8_21"},{"key":"16_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81\u201390. IEEE Computer Society Press (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587\u2013598. ACM (2011)","DOI":"10.1145\/1926385.1926453"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Ramsay, S.J., Neatherway, R.P., Ong, C.L.: A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of POPL 2014, pp. 61\u201372. ACM (2014)","DOI":"10.1145\/2535838.2535873"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of PEPM 2013, pp. 53\u201362. ACM (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-12736-1_19","volume-title":"Programming Languages and Systems","author":"T Terao","year":"2014","unstructured":"Terao, T., Kobayashi, N.: A ZDD-based efficient higher-order model checking algorithm. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 354\u2013371. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-12736-1_19"},{"key":"16_CR19","unstructured":"Terao, T., Tsukada, T., Kobayashi, N.: Higher-order model checking in direct style (2016). http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~terao\/papers\/aplas16.pdf"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-54830-7_12","volume-title":"Foundations of Software Science and Computation Structures","author":"T Tsukada","year":"2014","unstructured":"Tsukada, T., Kobayashi, N.: Complexity of model-checking call-by-value programs. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 180\u2013194. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54830-7_12"}],"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-47958-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T00:40:32Z","timestamp":1498351232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}