A Type System Equivalent to a Model Checker

ite-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. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification—Correctness proofs; Formal methods; Model checking General Terms: Verification Additional Key Words and Phrases: Type systems, model checking

• Type: Conference
• Year: 2005
• Where: ESOP
• Authors: Mayur Naik, Jens Palsberg
• Keywords: ESOP 2005, Ite-state Abstraction Scheme, Model Checking, Programming Languages, Type Systems