NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • Plaidypvs

    Plaidypvs (Properly Assured Implementation of Differential Dynamic Logic for Hybrid Program Verification and Specification) is a formal embedding of differential dynamic logic in the Prototype Verification System (PVS)[*]. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies.

    Applications of the Plaidypvs tool include: the development of a general framework for formalized reasoning of runtime assurance, a design-time architecture for safety critical systems, and an extension of Plaidypvs that can be used to verify temporal properties of hybrid systems.

    Plaidypvs is publicly available as part of the NASA PVS Library.


    The tag [*] identifies links that are outside the NASA domain