A type system equivalent to a model checker

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 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.

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.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 2: Torben Amtoft , Franklyn A. Turbak, Faithful Translations between Polyvariant Flows and Polymorphic Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.26-40, April 02, 2000
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 4: Anindya Banerjee, A modular, polyvariant and type-based closure analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.1-10, June 09-11, 1997, Amsterdam, The Netherlands
• 5: Mike Beaven , Ryan Stansifer, Explaining type errors in polymorphic languages, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.17-30, March–Dec. 1993 [doi>10.1145/176454.176460]
• 6: Dennis Brylow , Jens Palsberg, Deadline Analysis of Interrupt-Driven Software, IEEE Transactions on Software Engineering, v.30 n.10, p.634-655, October 2004 [doi>10.1109/TSE.2004.64]
• 7: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 8: Sagar Chaki , Sriram K. Rajamani , Jakob Rehof, Types as models: model checking message-passing programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.45-57, January 16-18, 2002, Portland, Oregon
• 9: Krishnendu Chatterjee , Di Ma , Rupak Majumdar , Tian Zhao , Thomas A. Henzinger , Jens Palsberg, Stack size analysis for interrupt-driven programs, Information and Computation, v.194 n.2, p.144-174, November 1, 2004 [doi>10.1016/j.ic.2004.06.001]
• 10: Olaf Chitil, Compositional explanation of types and algorithmic debugging of type errors, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 11: Patrick Cousot, Types as abstract interpretations, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-331, January 15-17, 1997, Paris, France [doi>10.1145/263699.263744]
• 12: Patrick Cousot , Radhia Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-25, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325699]
• 13: Mourad Debbabi , Abdelkader Benzakour , Béchir Ktari, A Synergy Between Model-Checking and Type Inference for the Verification of Value-Passing Higher-Order Processes, Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, p.214-230, January 04-08, 1999
• 14: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 15: Dominic Duggan , Frederick Bent, Explaining type inference, Science of Computer Programming, v.27 n.1, p.37-83, July 1996 [doi>10.1016/0167-6423(95)00007-0]
• 16: Cormac Flanagan , Stephen N. Freund, Type inference against races, Science of Computer Programming, v.64 n.1, p.140-165, January, 2007 [doi>10.1016/j.scico.2006.03.006]
• 17: Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040299]
• 18: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 19: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 20: 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.
• 21: Nevin Heintze, Control-Flow Analysis and Type Systems, Proceedings of the Second International Symposium on Static Analysis, p.189-206, September 25-27, 1995
• 22: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 23: 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.
• 24: Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.331-342, January 16-18, 2002, Portland, Oregon
• 25: Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512649]
• 26: Benjamin S. Lerner , Matthew Flower , Dan Grossman , Craig Chambers, Searching for type-error messages, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 27: Di Ma , Jens Palsberg, Bounding the stack size of interrupt-driven programs, Purdue University, West Lafayette, IN, 2004
• 28: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 29: Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.
• 30: Christian Mossin, Exact Flow Analysis, Proceedings of the 4th International Symposium on Static Analysis, p.250-264, September 08-10, 1997
• 31: Naik, M. 2004. A type system equivalent to a model checker. M.S. thesis, Purdue University.
• 32: Kedar S. Namjoshi, Certifying Model Checkers, Proceedings of the 13th International Conference on Computer Aided Verification, p.2-13, July 18-22, 2001
• 33: Kedar S. Namjoshi, Lifting Temporal Proofs through Abstractions, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.174-188, January 09-11, 2002
• 34: Jens Palsberg, Equality-based flow analysis versus recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.6, p.1251-1264, Nov. 1998 [doi>10.1145/295656.295662]
• 35: Jens Palsberg , Di Ma, A Typed Interrupt Calculus, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.291-310, September 09-12, 2002
• 36: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• 37: Jens Palsberg , Christina Pavlopoulou, From Polyvariant flow information to intersection and union types, Journal of Functional Programming, v.11 n.3, p.263-317, May 2001 [doi>10.1017/S095679680100394X]
• 38: Jens Palsberg , Scott Smith, Constrained types and their expressiveness, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.5, p.519-527, Sept. 1996 [doi>10.1145/232706.232715]
• 39: Doron Peled , Amir Pnueli , Lenore D. Zuck, From Falsification to Verification, Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, p.292-304, December 13-15, 2001
• 40: Doron Peled , Lenore Zuck, From model checking to a temporal proof, Proceedings of the 8th international SPIN workshop on Model checking of software, p.1-14, May 2001, Toronto, Ontario, Canada
• 41: David A. Schmidt , Bernhard Steffen, Program Analysis as Model Checking of Abstract Interpretations, Proceedings of the 5th International Symposium on Static Analysis, p.351-380, September 14-16, 1998
• 42: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 43: Bernhard Steffen, Data Flow Analysis as Model Checking, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.346-365, September 24-27, 1991
• 44: Li Tan , Rance Cleaveland, Evidence-Based Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.455-470, July 27-31, 2002
• 45: F. Tip , T. B. Dinesh, A slicing-based approach for locating type errors, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.1, p.5-55, Jan. 2001 [doi>10.1145/366378.366379]
• 46: David Walker , J. Gregory Morrisett, Alias Types for Recursive Data Structures, Selected papers from the Third International Workshop on Types in Compilation, p.177-206, September 21, 2000
• 47: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 48: Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking

General Terms:
Verification

Keywords:
Model checking, type systems