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

[PVS-ANNOUNCE] NASA PVS Library 6.0



The NASA PVS Library 6.0, for PVS 6.0, has been released:

  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library

This version of the library includes several upgrades, e.g.,

  structures: 
  - Added for-loops and iterations (for_iterate, for_examples).
  - Added Maybe and Unit types (Maybe, Unit).
  - Added a preliminary array theory tailored towards ground evaluation
(arrays).
  - Added a generic branch and bound algorithm (branch_and_bound).
  - Added a type of lists of n elements (listn).
  - Added array to list functions (array2list).

  interval_arith:
  - Added a formal proofs of Inclusion and Fundamental theorems of
interval arithmetic.
  - Completely redefined strategies for interval analysis.

  digraphs:
  - Revisited several definitions and lemmas.

Several additions to reals, analysis, vectors, etc. Furthermore, the
packages Extrategies and Field, which are now part of PVS, have been
completely revisited. These packages handle TCCs in a much better way.
Extrategies provides new strategy combinators for building strategies.

The whole library consists of 19162 lemmas from 40 different domains.

Enjoy it,

The NASA Langley Formal Methods Team