Michael Jones, PhD

The problem:
there are model checkers for multi threaded single process java programs. In java, its easy to define a multi process distributed program. There are no model checkers for multi-process distributed programs. Distributed means "programs that involve communication among multiple processes". and... RMI and encryption invoke native methods and "Supporting such native methods in a model checker is extremely problematic, because there is no general way for the model checker to save and restore their state."

The solution:
1. Centralization: "merge all processes into a single process"
2. RMI removal: replace RMI with normal method invocations.
3. Pseudo-crypto: replace cyptographic stuff with symbolic counterparts.

The limitations:
All three transformations rely on the assumption that the original program is not real-time and does not use reflection in a way that would detect the transformation's effects.

The details:
to be added later.

The results:
implementation is "mostly complete" Will be released as part of Bandera. First case study will be a scalable distributed voting system done as a class project. Should be done by SPIN 2001.

Relation to our work:
Assuming we make a model checker for C on a real time platform, there are some lessons to learn from this paper. First, as we expect, calls to native libraries are going to be difficult to model. We plan to not follow library calls into system code. This is similar to what gdb does if you "execute a funtion without descending into the function" I still think that's a fine idea.
Second, we are aiming for real time settings. Stoller and Liu deliberatly avoid real time. We may too in the end!