(* = offsite link)
Currently, there isn't much available for public download. (Students
working directly with the VFiasco team should contact Michael or
browse the internal project website.)
However, some tools of general interest have been made available:
- 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.
- 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++.
- This tool repairs a PVS proof (.prf) file that is the result of a
failed CVS merge (i.e., contains conflicts marked with
"<<<<<<< ======= >>>>>>>").
Last modified on
Last modified: Mon Jul 21 10:19:22 2003