PVS

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

pvs6/googleDrive





Comments