Formal methods and theorem proving using PVS

From VaVMURI

Return to workshop home

• Lecture slides (pdf)

Background reading

• A formalized theory for verifying convergence and stability of automata in PVS. S. Mitra and K. M. Chandy. In International Conference on Theorem Proving in Higher Order Logics, 2008.

Software

• PVS version 4.2
  • Follow instructions in INSTALL to install on your system. If you download the binary files, you should be able to put the PVS directory someplace, run bin/relocate, and then run pvs.
  • On OS X, I had to use 'pvs -emacs /Applications/Emacs.app/Contents/MacOS/Emacs' to get things to work --Murray 09:41, 16 September 2009 (PDT)
  • Alternative, run pvs -nw
• NASA Langley PVS library
  • Untar the library file in your PVS 4.2 home directory. Files will install in lib subdirectory
• pvslib.tgz - library for examples (compressed tar file)

Additional information