History of the Propel Toolset: Development of the Propel toolset for model checking C++ applications was started at NASA under funding from the Engineering for Complex Systems (ECS) program in 2001. The principal goal of this work was to develop tools for model checking NASA C++ flight software. The strategy for developing the tools was to leverage the existing research on program model checking, which had produced a research prototype tool, Java PathFinder (JPF), applicable to Java. The strategy of leveraging the prototype Java model checker was to be done by productizing the prototype and developing a translator from C++ to Java. JPF would then be applied to the translated C++ application.
It was recognized from the outset that not all of the C++ language and libraries could be mechanically translated into Java, and that there would likely be issues even with successfully translated code (for example, an increase in state space introduced by the translator). Nevertheless, this was deemed preferable to developing a completely new program model checker for C++. This work received continued funding from ECS through late 2004, at which time funding was terminated by a re-ordering of research priorities. By the time funding ended, a translation approach for the identified target subset of C++ had been designed and a prototype translator constructed. However, the prototype was not robust and no further funding was available to support its continued development.