Abstract
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 lends 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.
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 function types to capture flow sensitivity and intersection and union types to capture context sensitivity. Our result sheds light on the relationship between the two approaches, provides a methodology for studying their relative expressiveness, is a step towards sharing results between them, and motivates synergistic program analyses involving interplay between them.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Agarwal, R., Stoller, S.D.: Type inference for parameterized race-free java. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 149–160. Springer, Heidelberg (2004)
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM TOPLAS 15(4), 575–631 (1993)
Amtoft, T., Turbak, F.: Faithful translations between polyvariant flows and polymorphic types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 26–40. Springer, Heidelberg (2000)
Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Proceedings of POPL 2002, pp. 1–3 (2002)
Banerjee, A.: A modular, polyvariant and type-based closure analysis. In: Proceedings of ICFP 1997, pp. 1–10 (1997)
Beaven, M., Stansifer, R.: Explaining type errors in polymorphic languages. ACM LOPLAS 2(1-4), 17–30 (1993)
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–395 (2003)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: Model checking message-passing programs. In: Proceedings of POPL 2002, pp. 45–57 (2002)
Chitil, O.: Compositional explanation of types and algorithmic debugging of type errors. In: Proceedings of ICFP 2001, pp. 193–204 (2001)
Cousot, P.: Types as abstract interpretations. In: Proceedings of POPL 1997, pp. 316–331 (1997)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proceedings of POPL 2000, pp. 12–25 (2000)
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. 1548, pp. 214–230. Springer, Heidelberg (1998)
DeLine, R., Fahndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of PLDI 2001, pp. 59–69 (2001)
Duggan, D., Bent, F.: Explaining type inference. Science of Computer Programming 27(1), 37–83 (1996)
Flanagan, C., Freund, S.N.: Type inference against races. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 116–132. Springer, Heidelberg (2004)
Flanagan, C., Freund, S.N., Lifshin, M.: Type inference for atomicity. In: Proceedings of TLDI 2005 (January 2005)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of PLDI 2002, pp. 1–12 (2002)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Haack, C., Wells, J.B.: Type error slicing in implicitly typed higher-order languages. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 284–301. Springer, Heidelberg (2003)
Heintze, N.: Control-flow analysis and type systems. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 189–206. Springer, Heidelberg (1995)
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. 2404, pp. 526–538. Springer, Heidelberg (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proceedings of POPL 2002, pp. 331–342 (2002)
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–57 (1986)
Ma, D.: Bounding the Stack Size of Interrupt-Driven Programs. PhD thesis, Purdue University (2004)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proceedings of ICFP 2003 (2003)
Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348–375 (1978)
Mossin, C.: Exact flow analysis. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 250–264. Springer, Heidelberg (1997)
Naik, M.: A type system equivalent to a model checker. Master’s thesis, Purdue University (2004)
Naik, M., Palsberg, J.: A type system equivalent to a model checker. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 374–388. Springer, Heidelberg (2005); Full version with proofs available at http://www.cs.stanford.edu/~mhn/pubs/esop05.html
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–12. Springer, Heidelberg (2001)
Namjoshi, K.S.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 174–188. Springer, Heidelberg (2002)
Palsberg, J., Pavlopoulou, C.: From polyvariant flow information to intersection and union types. Journal of Functional Programming 11(3), 263–317 (2001)
Palsberg, J.: Equality-based flow analysis versus recursive types. ACM TOPLAS 20(6), 1251–1264 (1998)
Palsberg, J., Ma, D.: A typed interrupt calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 291–310. Springer, Heidelberg (2002)
Palsberg, J., O’Keefe, P.M.: A type system equivalent to flow analysis. ACM TOPLAS 17(4), 576–599 (1995)
Palsberg, J., Smith, S.: Constrained types and their expressiveness. ACM TOPLAS 18(5), 519–527 (1996)
Peled, D., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001)
Peled, D., Zuck, L.D.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 1–14. Springer, Heidelberg (2001)
Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)
Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Proceedings of POPL 1998, pp. 38–48 (1998)
Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–364. Springer, Heidelberg (1991)
Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002)
Tip, F., Dinesh, T.B.: A slicing-based approach for locating type errors. ACM TOSEM 10(1), 5–55 (2001)
Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 177–206. Springer, Heidelberg (2001)
Wand, M.: Finding the source of type errors. In: Proceedings of POPL 1986, pp. 38–43 (1986)
Xi, H.: Imperative programming with dependent types. In: Proceedings of LICS 2000, pp. 375–387 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Naik, M., Palsberg, J. (2005). A Type System Equivalent to a Model Checker. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)