A Type System Equivalent to a Model Checker

11 years 7 months ago
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
Mayur Naik, Jens Palsberg
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ESOP
Authors Mayur Naik, Jens Palsberg
Comments (0)