Mayur Naik and Jens Palsberg:
Type systems and model checking are two approaches to finding bugs in software. Are they equally powerful? On the surface, they are quite different: type checking works on the program itself, often in a modular fashion, while model checking works on a model of the program. Type soundness ensures that all reachable program states satisfy a certain property provided the program is well typed, while model-checking soundness guarantees the same without any assumptions about types. Thus, model checking seems to be more powerful than type checking: Type soundness essentially says that type checking implies model checking, but there are not many cases where the converse holds.…In this paper, we present a type system that is equivalent to model checking.
Comments
