Back to main page
V E R I F I E D
Fiasco
Site Navigation: (* = offsite link)

Quick links:

Download

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 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 "<<<<<<< ======= >>>>>>>").


Last modified on Last modified: Mon Jul 21 10:19:22 2003


Hendrik Tews <tews@tcs.inf.tu-dresden.de>
Michael Hohmuth <hohmuth@inf.tu-dresden.de>