[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: client access to PVS system.

As part of his master's thesis Jens Knappmann developed a Tcl/Tk
interface to his prototype of a refinement calculator in PVS. The
interface process is started from within emacs similarly to, e.g., the
proof tree display of PVS and is linked to the pvs buffer via named
pipes. At URL


you'll find a rudimentary description of the tool as well as links to
the source code and the documentation. Chapter 7 of the latter
describes the interface and how it is linked to PVS.