BackendSubsystemsExplanation

Several new "backend" subsystems have been developed with MOBIUS resources. These systems are "backend" in the sense that they are used by many other subsystems and are deeply embedded in other tools, thus they are mainly interfaced via APIs and are heavily reused.

These subsystems include automated theorem provers, verification condition generators, specification generators, and intermediate representations for reasoning. All of these subsystems are used within the Mobius PVE, many for several purposes.

Version: 1 Time: Fri Mar 28 16:11:35 2008 Author: dcochran (dcochran) IP: 193.1.132.32