Model Checking SAFM: Our intention was to use JPF for program model checking of these properties. The SAFM code was partially translated to Java using Propel, a C++-to-Java translator that was being developed for the purpose of bringing model checking and other program analyses to C++. Application of the model checker was limited for the reasons. However, an experiment was performed in model checking a portion of SAFM that contained an error found by inspection, but that had not been revealed by the SAFM test suite. A D4V change, that of exploiting polymorphism, made the error more apparent. A property revealing the error was formulated and model checked on the original translated code and the code after performing the D4V change. JPF’s choice generators were used to completely cover an input space relevant to the portion. On average, JPF used 25% less time and 13% less memory to check the code that was modified based on the identified D4V opportunity, even though the space explored was the same, because the paths to be checked to detect the error were shorter.