[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