[Prev][Next][Index][Thread]
Thesis announcement: A Type System Equivalent to Model Checking
I am pleased to announce the availability of my M.S. thesis from Purdue
University:
A Type System Equivalent To Model Checking
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 it
self, 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 essential
ly says that type checking implies model checking, but there are
not many cases where the converse holds.
In this thesis, we present a type system that is equivalent to
model checking. We work with a simple model checking problem,
namely, deadline analysis: For an interrupt-driven program, will
every interrupt be handled within the deadline? For the inter
rupt calculus of Palsberg and Ma, we construct finite-state mod
els of programs that enable straightforward model checking for
deadline analysis. We then present a type system which type
checks exactly those programs that are accepted by the model
checker. We use singleton types and, more significantly, inter
section and union types containing information about time. Our
result sheds light on the relationship between type systems and
model checking, and it provides a means of explaining to the pro
grammer why a run of a model checker succeeded and found no bugs.
The reason is that the proof of equivalence is constructive and
therefore enables type inference by model checking. Thus, a tool
can output a version of the program that is annotated with timing
information.
Advisor: Prof. Jens Palsberg
The thesis is available at:
http://www.cs.purdue.edu/homes/mnaik/pubs/tsemc.html
Comments and suggestions are most welcome.
-- Mayur Naik