Plaidypvs

Plaidypvs (A 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.

Publications

• Slagel, J. T., Moscato, M., White, L., Muñoz, C., Balachandran, S., & Dutle, A. Embedding Differential Dynamic Logic in PVS. In Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023.
• White, L., Titolo, L., & Slagel, J. T. Embedding Differential Temporal Dynamic Logic in PVS. In 29th International Conference on Types for Proofs and Programs TYPES 2023 Abstracts, 2023.
• Slagel, J. T., Muñoz, C., Balachandran, S., Moscato, M., Dutle, A., Masci, P., & White, L. Towards an implementation of differential dynamic logic in PVS. In Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2022.

The tag identifies links that are outside the NASA domain