{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:05:04Z","timestamp":1755907504995,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T00:00:00Z","timestamp":1581984000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,2,18]]},"DOI":"10.1145\/3384544.3384587","type":"proceedings-article","created":{"date-parts":[[2020,5,4]],"date-time":"2020-05-04T03:58:24Z","timestamp":1588564704000},"page":"357-363","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Static Code Analysis Using Refinement Types based on Design by Contract"],"prefix":"10.1145","author":[{"given":"Koji","family":"Ishii","sequence":"first","affiliation":[{"name":"Tokyo Institute of Technology, Ookayama, Meguro Tokyo, JAPAN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shin-ya","family":"Nishizaki","sequence":"additional","affiliation":[{"name":"Tokyo Institute of Technology, Ookayama, Meguro Tokyo, JAPAN"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"e_1_3_2_1_3_1","first-page":"171","volume-title":"CAV 2011","volume":"6806","author":"Barrett C.","year":"2011","unstructured":"Barrett, C., Conway, C. L., Deters, M., Hadarean, L., and Jovanovi\u0107, D. CVC4. In Computer Aided Verification, CAV 2011 (2011), vol. 6806 of Lecture Notes in Computer Science, Springer, pp. 171--177."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_5_1","first-page":"502","volume-title":"An Extensible SAT-solver. In SAT 2003","author":"E\u00e9n N.","year":"2004","unstructured":"E\u00e9n, N., and S\u00f6rensson, N. An Extensible SAT-solver. In SAT 2003 (2004), Lecture Notes in Computer Science, Springer-Verlag, pp. 502---518."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_9_1","volume-title":"Hybrid type checking. ACM Transaction on Programming Languages and Systems (TOPLAS) 32, 2 (January","author":"Knowles K.","year":"2010","unstructured":"Knowles, K., and Flanagan, C. Hybrid type checking. ACM Transaction on Programming Languages and Systems (TOPLAS) 32, 2 (January 2010)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-4-431-54436-4_3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/129093"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCIT.2010.5664903"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35864-7_10"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"}],"event":{"name":"ICSCA 2020: 2020 9th International Conference on Software and Computer Applications","acronym":"ICSCA 2020","location":"Langkawi Malaysia"},"container-title":["Proceedings of the 2020 9th International Conference on Software and Computer Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3384544.3384587","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3384544.3384587","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:19:21Z","timestamp":1755839961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3384544.3384587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,18]]},"references-count":17,"alternative-id":["10.1145\/3384544.3384587","10.1145\/3384544"],"URL":"https:\/\/doi.org\/10.1145\/3384544.3384587","relation":{},"subject":[],"published":{"date-parts":[[2020,2,18]]},"assertion":[{"value":"2020-04-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}