[TYPES/announce] Announcing the release of PVS 7.1.

Sam Owre owre at csl.sri.com
Wed Nov 18 17:21:03 EST 2020


Hi All,

We are pleased to announce the release of PVS version 7.1.  This has many
new features; read the release notes for details.  Here we list a summary of
the highlights.

- The http://pvs.csl.sri.com web site has been updated, with a more modern
  look, and simplified access to the downloads, manuals, etc.

- A new API is under development, based on XML-RPC.
   
- NASA has developed a new VSCode GUI (https://github.com/nasa/vscode-pvs),
  using the XML-RPC API.  This is still a work in progress, but is already
  usable for those who prefer an alternative to Emacs.  This is not a
  replacement, the Emacs GUI works as usual, and will continue to be supported
  for the foreseeable future.

- The library mechanism has been simplified and improved, allowing changes to
  be made to libraries without the need to change contexts, which makes
  development and use of libraries much easier and faster.

- Theory interpretations have been significantly improved.

- Yices 1 and 2 have now been included in PVS 7.1, so the yices and yices2
  proof commands work out of the box.

- There are a number of minor language changes, e.g., "0 < x <= n" is a valid
  expression.

- TCCs have been cleaned up.  In general, all TCCs have an associated location,
  even when terms have been created for typechecking purposes.  TCCs have also
  been "normalized", and are presented in a more natural form.

Please enjoy!


More information about the Types-announce mailing list