[TYPES/announce] [fm-announcements] Release of NASA PVS Library v7.1

[Munoz, Cesar (LARC-D320) via fm-announcements]

The Formal Methods Team at NASA Langley Research Center and the National Institute of Aerospace is pleased to announce the release of the NASA PVS Library (NASALib) v7.1 (https://github.com/nasa/pvslib). NASALib v7.1 is fully compatible with PVS 7.1 (https://pvs.csl.sri.com), the recently released version of the Prototype Verification System (PVS). 
  
NASALib is a continuing collaborative effort that has spanned over 3 decades, to aid in research related to theorem proving  sponsored by NASA (https://shemesh.larc.nasa.gov/fm/pvs/). It consists of a collection of formal developments written in PVS, contributed by SRI, NASA, NIA, and the PVS community, and maintained by the NASA/NIA Formal Methods Team at LaRC. Currently, NASALib v7.1 includes 53 developments and almost 30k formally proved lemmas and theorems. 

In addition to NASALib v7.1, the following developments have been updated to PVS 7.1 and are publicly available  under NASA's Open Source Agreement:

* vscode-pvs (https://shemesh.larc.nasa.gov/fm/VSCode-PVS/): A Visual Studio Code (https://code.visualstudio.com/) extension that provides a modern integrated development environment for PVS.

* PRECiSA (https://shemesh.larc.nasa.gov/fm/PRECiSA): A static analysis tool that generates provably correct round-off error bounds of floating-point programs.

* PolyCARP (https://shemesh.larc.nasa.gov/fm/PolyCARP): A collection of formally verified algorithms for computations with polygons.

* CPR* (https://shemesh.larc.nasa.gov/fm/CPR): Formally verified implementations in C (fixed-point and floating-point) of ADS-B's Compact Position Reporting algorithms. CPR* is the reference implementation of CPR in the international standard ED-102B/DO-260C.

* DAIDALUS (https://shemesh.larc.nasa.gov/fm/DAIDALUS): A collection of formally verified algorithms for a detect and avoid concept that supports the integration of Unmanned Aircraft Systems (UAS) into the National Airspace System (NAS). DAIDALUS is the reference implementation of functional requirements for Detect and Avoid of UAS in the US standard DO-365A.

Enjoy,

The NASA/NIA Formal Methods Team at LaRC
https://shemesh.larc.nasa.gov/fm


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 7429 bytes
Desc: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20201120/f1dacd33/attachment-0001.p7s>
-------------- next part --------------
---
To opt-out from this mailing list, send an email to

fm-announcements-request at lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner at lists.nasa.gov