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
smime.p7s
Description: S/MIME cryptographic signature
--- To opt-out from this mailing list, send an email to fm-announcements-requ...@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-ow...@lists.nasa.gov
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
