We started a completely new PVS
design of GDFM
(Google Drive Formal Model) on 6 February 2015, with the aim of obtaining crystal clear proof obligations (TCCs), and elegant proofs. There is currently one library only, but we anticipate two:
- basics: some basic extension of PVS 6 prelude or theories available from PVS 6 standard libraries, empty for the moment;
- googleDrive: the formal model itself, that will eventually use basics library.
Most recent dump and corresponding proof status
PVS 6 development directory