{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T12:52:22Z","timestamp":1726059142070},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030355395"},{"type":"electronic","value":"9783030355401"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-35540-1_1","type":"book-chapter","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:01:29Z","timestamp":1574035289000},"page":"1-18","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Bounded Model Checking Technique for Higher-Order Programs"],"prefix":"10.1007","author":[{"given":"Yu-Yang","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-36577-X_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Amla","year":"2003","unstructured":"Amla, N., Kurshan, R., McMillan, K.L., Medel, R.: Experimental analysis of different techniques for bounded model checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 34\u201348. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36577-X_4"},{"key":"1_CR2","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, DIKU, University of Copenhagen, May 1994. (DIKU report 94\/19)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/390016.808445","volume":"10","author":"RS Boyer","year":"1975","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.: SELECT-a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not. 10, 234\u2013245 (1975)","journal-title":"ACM SIGPLAN Not."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. In: PACMPL, 2(POPL), pp. 11:1\u201311:28 (2018)","DOI":"10.1145\/3158099"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"1_CR7","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 Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F.S., Jackson, D.: Modular verification of code with SAT. In: Pollock, L.L., Pezz\u00e8, M. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, 17\u201320 July 2006, pp. 109\u2013120. ACM (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, Dubrovnik, Croatia, 3\u20137 September 2007, pp. 195\u2013204. ACM (2007)","DOI":"10.1145\/1287624.1287653"},{"issue":"7","key":"1_CR10","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circ. Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"issue":"9","key":"1_CR11","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1109\/TSE.2013.15","volume":"39","author":"JP Galeotti","year":"2013","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283\u20131307 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"1_CR12","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1109\/TSE.1977.231144","volume":"SE-3","author":"W.E. Howden","year":"1977","unstructured":"Howden, W.E.: Symbolic testing and the DISSECT symbolic evaluation system. IEEE Trans. Softw. Eng. SE-3, 266\u2013278 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"King, J.C.: A new approach to program testing. In: Proceedings of the International Conference on Reliable Software, pp. 228\u2013233. ACM (1975)","DOI":"10.1145\/800027.808444"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 416\u2013428. ACM, New York (2009)","DOI":"10.1145\/1480881.1480933"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993498.1993525"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-54862-8_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Morse","year":"2014","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405\u2013407. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_31"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: Rubicon: bounded verification of web applications. In: Tracz, W., Robillard, M.P., Bultan, T. (eds.) 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT\/FSE 2012, Cary, NC, USA, 11\u201316 November 2012, p. 60. ACM (2012)","DOI":"10.1145\/2393596.2393667"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Nguyen, P.C., Horn, D.V. (eds.) Relatively complete counterexamples for higher-order programs. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 446\u2013456. ACM (2015)","DOI":"10.1145\/2737924.2737971"},{"key":"1_CR19","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 81\u201390, August 2006"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82\u201397. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11513988_9"},{"issue":"4","key":"1_CR21","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. High. Order Symb. Comput. 11(4), 363\u2013397 (1998)","journal-title":"High. Order Symb. Comput."},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-662-54580-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Rocha","year":"2017","unstructured":"Rocha, W., Rocha, H., Ismail, H., Cordeiro, L., Fischer, B.: DepthK: A k-induction verifier based on invariant inference for C programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 360\u2013364. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54580-5_23"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Albert, E., Mu, S. (eds.) Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, pp. 53\u201362. ACM (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"1_CR24","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, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-12736-1_19"},{"issue":"6","key":"1_CR25","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/2666356.2594340","volume":"49","author":"Emina Torlak","year":"2014","unstructured":"Torlak, E., Bod\u00edk, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09\u201311 June 2014, pp. 530\u2013541. ACM (2014)","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-35540-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:21:41Z","timestamp":1574036501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-35540-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030355395","9783030355401"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-35540-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www4.comp.polyu.edu.hk\/~csguannan\/setta19\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}