Download

However, some tools of general interest have been made available:

CCSL compiler

CCSL - The Coalgebraic Class Specification Language - is a specification language that combines both algebraic and coalgebraic elements. The CCSL compiler translates CCSL specifications into higher-order logic either for PVS or for for Isabelle/HOL (in new style Isar syntax). After translation the theorem prover can be used to examine the specification, built models, construct refinements, and much more.

C++ Annotator

A C++ library for parsing C++ source code, including name and type analysis. This library will evolve into our C++ semantics compiler. C++ Annotator is based on OpenC++.

prfmerge

This tool repairs a PVS proof (.prf) file that is the result of a failed CVS merge (i.e., contains conflicts marked with "<<<<<<< ======= >>>>>>>").