{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:38:15Z","timestamp":1750307895406,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2008,8,1]],"date-time":"2008-08-01T00:00:00Z","timestamp":1217548800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["112628"],"award-info":[{"award-number":["112628"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,8]]},"abstract":"<jats:p>Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a semantic and whole-program style. This difference between the two approaches makes them complementary to each other: type systems are good at explaining why a program was accepted while model checkers are good at explaining why a program was rejected.<\/jats:p>\n          <jats:p>We present a type system that is equivalent to a model checker for verifying temporal safety properties of imperative programs. The model checker is natural and may be instantiated with any finite-state abstraction scheme such as predicate abstraction. The type system, which is also parametric, type checks exactly those programs that are accepted by the model checker. It uses a variant of function types to capture flow sensitivity and intersection and union types to capture context sensitivity. Our result sheds light on the relationship between type systems and model checking, provides a methodology for studying their relative expressiveness, is a step towards sharing results between the two approaches, and motivates synergistic program analyses involving interplay between them.<\/jats:p>","DOI":"10.1145\/1387673.1387678","type":"journal-article","created":{"date-parts":[[2008,9,4]],"date-time":"2008-09-04T12:51:35Z","timestamp":1220532695000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A type system equivalent to a model checker"],"prefix":"10.1145","volume":"30","author":[{"given":"Mayur","family":"Naik","sequence":"first","affiliation":[{"name":"Intel Research, Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"UCLA, Los Angeles, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,9,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"volume-title":"Proceedings of the 14th European Symposium on Programming. Springer, 26--40","author":"Amtoft T.","key":"e_1_2_1_2_1","unstructured":"Amtoft , T. and Turbak , F . 2000. Faithful translations between polyvariant flows and polymorphic types . In Proceedings of the 14th European Symposium on Programming. Springer, 26--40 . Amtoft, T. and Turbak, F. 2000. Faithful translations between polyvariant flows and polymorphic types. In Proceedings of the 14th European Symposium on Programming. Springer, 26--40."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258951"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/176454.176460"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.64"},{"volume-title":"Proceedings of the 25th International on Software Engineering. IEEE Computer Society Press, 385--395","author":"Chaki S.","key":"e_1_2_1_7_1","unstructured":"Chaki , S. , Clarke , E. M. , Groce , A. , Jha , S. , and Veith , H . 2003. Modular verification of software components in C . In Proceedings of the 25th International on Software Engineering. IEEE Computer Society Press, 385--395 . Chaki, S., Clarke, E. M., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In Proceedings of the 25th International on Software Engineering. IEEE Computer Society Press, 385--395."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503278"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1709463.1709555"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507659"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325699"},{"volume-title":"Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology. Springer, 214--230","author":"Debbabi M.","key":"e_1_2_1_13_1","unstructured":"Debbabi , M. , Benzakour , A. , and Ktari , B . 1999. A synergy between model-checking and type inference for the verification of value-passing higher-order processes . In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology. Springer, 214--230 . Debbabi, M., Benzakour, A., and Ktari, B. 1999. A synergy between model-checking and type inference for the verification of value-passing higher-order processes. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology. Springer, 214--230."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00007-0"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.006"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040294.1040299"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification. Springer, 72--83","author":"Graf S.","key":"e_1_2_1_19_1","unstructured":"Graf , S. and Saidi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the 9th International Conference on Computer-Aided Verification. Springer, 72--83 . Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer-Aided Verification. Springer, 72--83."},{"volume-title":"Proceedings of the 12th European Symposium on Programming. Springer, 284--301","author":"Haack C.","key":"e_1_2_1_20_1","unstructured":"Haack , C. and Wells , J. B . 2003. Type error slicing in implicitly typed higher-order languages . In Proceedings of the 12th European Symposium on Programming. Springer, 284--301 . Haack, C. and Wells, J. B. 2003. Type error slicing in implicitly typed higher-order languages. In Proceedings of the 12th European Symposium on Programming. Springer, 284--301."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.760061"},{"volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 526--538","author":"Henzinger T. A.","key":"e_1_2_1_22_1","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , Necula , G. C. , Sutre , G. , and Weimer , W . 2002. Temporal-safety proofs for systems code . In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 526--538 . Henzinger, T. A., Jhala, R., Majumdar, R., Necula, G. C., Sutre, G., and Weimer, W. 2002. Temporal-safety proofs for systems code. In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 526--538."},{"volume-title":"Proceedings of the 10th International SPIN Workshop on Model Checking Software. Springer, 235--239","author":"Henzinger T. A.","key":"e_1_2_1_23_1","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , and Sutre , G . 2003. Software verification with Blast . In Proceedings of the 10th International SPIN Workshop on Model Checking Software. Springer, 235--239 . Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with Blast. In Proceedings of the 10th International SPIN Workshop on Model Checking Software. Springer, 235--239."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512649"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250783"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944725"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647166.717967"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734121"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696199"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295662"},{"volume-title":"Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. Springer, 291--310","author":"Palsberg J.","key":"e_1_2_1_35_1","unstructured":"Palsberg , J. and Ma , D . 2002. A typed interrupt calculus . In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. Springer, 291--310 . Palsberg, J. and Ma, D. 2002. A typed interrupt calculus. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. Springer, 291--310."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/210184.210187"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680100394X"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/232706.232715"},{"volume-title":"Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 292--304","author":"Peled D.","key":"e_1_2_1_39_1","unstructured":"Peled , D. , Pnueli , A. , and Zuck , L. D . 2001. From falsification to verification . In Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 292--304 . Peled, D., Pnueli, A., and Zuck, L. D. 2001. From falsification to verification. In Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 292--304."},{"volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 1--14","author":"Peled D.","key":"e_1_2_1_40_1","unstructured":"Peled , D. and Zuck , L. D . 2001. From model checking to a temporal proof . In Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 1--14 . Peled, D. and Zuck, L. D. 2001. From model checking to a temporal proof. In Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 1--14."},{"volume-title":"Proceedings of the 5th International Symposium on Static Analysis. Springer, 351--380","author":"Schmidt D.","key":"e_1_2_1_41_1","unstructured":"Schmidt , D. and Steffen , B . 1998. Program analysis as model checking of abstract interpretations . In Proceedings of the 5th International Symposium on Static Analysis. Springer, 351--380 . Schmidt, D. and Steffen, B. 1998. Program analysis as model checking of abstract interpretations. In Proceedings of the 5th International Symposium on Static Analysis. Springer, 351--380."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268950"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670930"},{"volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 455--470","author":"Tan L.","key":"e_1_2_1_44_1","unstructured":"Tan , L. and Cleaveland , R . 2002. Evidence-based model checking . In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 455--470 . Tan, L. and Cleaveland, R. 2002. Evidence-based model checking. In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 455--470."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/366378.366379"},{"volume-title":"Proceedings of the 3rd International Workshop on Types in Compilation. Springer, 177--206","author":"Walker D.","key":"e_1_2_1_46_1","unstructured":"Walker , D. and Morrisett , G . 2001. Alias types for recursive data structures . In Proceedings of the 3rd International Workshop on Types in Compilation. Springer, 177--206 . Walker, D. and Morrisett, G. 2001. Alias types for recursive data structures. In Proceedings of the 3rd International Workshop on Types in Compilation. Springer, 177--206."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512648"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 375--387","author":"Xi H.","year":"2000","unstructured":"Xi , H. 2000 . Imperative programming with dependent types . In Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 375--387 . Xi, H. 2000. Imperative programming with dependent types. In Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 375--387."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1387673.1387678","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1387673.1387678","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:26Z","timestamp":1750258046000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1387673.1387678"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,8]]}},"alternative-id":["10.1145\/1387673.1387678"],"URL":"https:\/\/doi.org\/10.1145\/1387673.1387678","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2008,8]]},"assertion":[{"value":"2005-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}