{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:53:38Z","timestamp":1725573218329},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540254355"},{"type":"electronic","value":"9783540319870"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31987-0_26","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T13:42:00Z","timestamp":1292852520000},"page":"374-388","source":"Crossref","is-referenced-by-count":11,"title":["A Type System Equivalent to a Model Checker"],"prefix":"10.1007","author":[{"given":"Mayur","family":"Naik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-24622-0_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Agarwal","year":"2004","unstructured":"Agarwal, R., Stoller, S.D.: Type inference for parameterized race-free java. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 149\u2013160. Springer, Heidelberg (2004)"},{"issue":"4","key":"26_CR2","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R.M. Amadio","year":"1993","unstructured":"Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM TOPLAS\u00a015(4), 575\u2013631 (1993)","journal-title":"ACM TOPLAS"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/3-540-46425-5_2","volume-title":"Programming Languages and Systems","author":"T. Amtoft","year":"2000","unstructured":"Amtoft, T., Turbak, F.: Faithful translations between polyvariant flows and polymorphic types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 26\u201340. Springer, Heidelberg (2000)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Proceedings of POPL 2002, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Banerjee, A.: A modular, polyvariant and type-based closure analysis. In: Proceedings of ICFP 1997, pp. 1\u201310 (1997)","DOI":"10.1145\/258948.258951"},{"issue":"1-4","key":"26_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/176454.176460","volume":"2","author":"M. Beaven","year":"1993","unstructured":"Beaven, M., Stansifer, R.: Explaining type errors in polymorphic languages. ACM LOPLAS\u00a02(1-4), 17\u201330 (1993)","journal-title":"ACM LOPLAS"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proceedings of ICSE 2003, May 2003, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: Model checking message-passing programs. In: Proceedings of POPL 2002, pp. 45\u201357 (2002)","DOI":"10.1145\/503272.503278"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Chitil, O.: Compositional explanation of types and algorithmic debugging of type errors. In: Proceedings of ICFP 2001, pp. 193\u2013204 (2001)","DOI":"10.1145\/507635.507659"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Types as abstract interpretations. In: Proceedings of POPL 1997, pp. 316\u2013331 (1997)","DOI":"10.1145\/263699.263744"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proceedings of POPL 2000, pp. 12\u201325 (2000)","DOI":"10.1145\/325694.325699"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/3-540-49253-4_17","volume-title":"Algebraic Methodology and Software Technology","author":"M. Debbabi","year":"1998","unstructured":"Debbabi, M., Benzakour, A., Ktari, K.: A synergy between model-checking and type inference for the verification of value-passing higher-order processes. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 214\u2013230. Springer, Heidelberg (1998)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"DeLine, R., Fahndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of PLDI 2001, pp. 59\u201369 (2001)","DOI":"10.1145\/378795.378811"},{"issue":"1","key":"26_CR14","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0167-6423(95)00007-0","volume":"27","author":"D. Duggan","year":"1996","unstructured":"Duggan, D., Bent, F.: Explaining type inference. Science of Computer Programming\u00a027(1), 37\u201383 (1996)","journal-title":"Science of Computer Programming"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-27864-1_11","volume-title":"Static Analysis","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.N.: Type inference against races. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 116\u2013132. Springer, Heidelberg (2004)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Lifshin, M.: Type inference for atomicity. In: Proceedings of TLDI 2005 (January 2005)","DOI":"10.1145\/1040294.1040299"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of PLDI 2002, pp. 1\u201312 (2002)","DOI":"10.1145\/512529.512531"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-36575-3_20","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2003","unstructured":"Haack, C., Wells, J.B.: Type error slicing in implicitly typed higher-order languages. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 284\u2013301. Springer, Heidelberg (2003)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60360-3_40","volume-title":"Static Analysis","author":"N. Heintze","year":"1995","unstructured":"Heintze, N.: Control-flow analysis and type systems. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 189\u2013206. Springer, Heidelberg (1995)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proceedings of POPL 2002, pp. 331\u2013342 (2002)","DOI":"10.1145\/503272.503303"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Johnson, G.F., Walz, J.A.: A maximum flow approach to anomaly isolation in unification-based incremental type inference. In: Proceedings of POPL 1986, pp. 44\u201357 (1986)","DOI":"10.1145\/512644.512649"},{"key":"26_CR25","unstructured":"Ma, D.: Bounding the Stack Size of Interrupt-Driven Programs. PhD thesis, Purdue University (2004)"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proceedings of ICFP 2003 (2003)","DOI":"10.1145\/944705.944725"},{"key":"26_CR27","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences\u00a017, 348\u2013375 (1978)","journal-title":"Journal of Computer and System Sciences"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/BFb0032746","volume-title":"Static Analysis","author":"C. Mossin","year":"1997","unstructured":"Mossin, C.: Exact flow analysis. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 250\u2013264. Springer, Heidelberg (1997)"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Naik, M.: A type system equivalent to a model checker. Master\u2019s thesis, Purdue University (2004)","DOI":"10.1007\/978-3-540-31987-0_26"},{"key":"26_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-31987-0_26","volume-title":"Programming Languages and Systems","author":"M. Naik","year":"2005","unstructured":"Naik, M., Palsberg, J.: A type system equivalent to a model checker. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 374\u2013388. Springer, Heidelberg (2005); Full version with proofs available at http:\/\/www.cs.stanford.edu\/~mhn\/pubs\/esop05.html"},{"key":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 2\u201312. Springer, Heidelberg (2001)"},{"key":"26_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-36384-X_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2002","unstructured":"Namjoshi, K.S.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 174\u2013188. Springer, Heidelberg (2002)"},{"issue":"3","key":"26_CR33","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1017\/S095679680100394X","volume":"11","author":"J. Palsberg","year":"2001","unstructured":"Palsberg, J., Pavlopoulou, C.: From polyvariant flow information to intersection and union types. Journal of Functional Programming\u00a011(3), 263\u2013317 (2001)","journal-title":"Journal of Functional Programming"},{"issue":"6","key":"26_CR34","doi-asserted-by":"publisher","first-page":"1251","DOI":"10.1145\/295656.295662","volume":"20","author":"J. Palsberg","year":"1998","unstructured":"Palsberg, J.: Equality-based flow analysis versus recursive types. ACM TOPLAS\u00a020(6), 1251\u20131264 (1998)","journal-title":"ACM TOPLAS"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45739-9_18","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J. Palsberg","year":"2002","unstructured":"Palsberg, J., Ma, D.: A typed interrupt calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 291\u2013310. Springer, Heidelberg (2002)"},{"issue":"4","key":"26_CR36","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/210184.210187","volume":"17","author":"J. Palsberg","year":"1995","unstructured":"Palsberg, J., O\u2019Keefe, P.M.: A type system equivalent to flow analysis. ACM TOPLAS\u00a017(4), 576\u2013599 (1995)","journal-title":"ACM TOPLAS"},{"issue":"5","key":"26_CR37","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1145\/232706.232715","volume":"18","author":"J. Palsberg","year":"1996","unstructured":"Palsberg, J., Smith, S.: Constrained types and their expressiveness. ACM TOPLAS\u00a018(5), 519\u2013527 (1996)","journal-title":"ACM TOPLAS"},{"key":"26_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D. Peled","year":"2001","unstructured":"Peled, D., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 292\u2013304. Springer, Heidelberg (2001)"},{"key":"26_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45139-0_1","volume-title":"Model Checking Software","author":"D. Peled","year":"2001","unstructured":"Peled, D., Zuck, L.D.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 1\u201314. Springer, Heidelberg (2001)"},{"key":"26_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"D. Schmidt","year":"1998","unstructured":"Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol.\u00a01503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"26_CR41","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Proceedings of POPL 1998, pp. 38\u201348 (1998)","DOI":"10.1145\/268946.268950"},{"key":"26_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B. Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 346\u2013364. Springer, Heidelberg (1991)"},{"key":"26_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Computer Aided Verification","author":"L. Tan","year":"2002","unstructured":"Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 455\u2013470. Springer, Heidelberg (2002)"},{"issue":"1","key":"26_CR44","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/366378.366379","volume":"10","author":"F. Tip","year":"2001","unstructured":"Tip, F., Dinesh, T.B.: A slicing-based approach for locating type errors. ACM TOSEM\u00a010(1), 5\u201355 (2001)","journal-title":"ACM TOSEM"},{"key":"26_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-45332-6_7","volume-title":"Types in Compilation","author":"D. Walker","year":"2001","unstructured":"Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol.\u00a02071, pp. 177\u2013206. Springer, Heidelberg (2001)"},{"key":"26_CR46","doi-asserted-by":"crossref","unstructured":"Wand, M.: Finding the source of type errors. In: Proceedings of POPL 1986, pp. 38\u201343 (1986)","DOI":"10.1145\/512644.512648"},{"key":"26_CR47","unstructured":"Xi, H.: Imperative programming with dependent types. In: Proceedings of LICS 2000, pp. 375\u2013387 (2000)"}],"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-540-31987-0_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:33:21Z","timestamp":1605742401000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}