Responsible for reworking the verification condition generator interface to ESC/Java. In particular, two mechanisms for introducing new theorem provers have been defined:

  • new plugin theorem provers may be introduced by implementing a single interface
  • new plugin theorem provers may be specified using XSLT stylesheets to transform an output XML stream from the verification condition generator