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.

Publications

• Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz, A Temporal Differential Dynamic Logic Formal Embedding, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), London, UK, 2024. BibTeX Reference.
• J Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran, and Aaron Dutle, Embedding Differential Dynamic Logic in PVS,Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023. BibTeX Reference.
• Lauren White, Laura Titolo, J. Tanner Slagel, Embedding Differential Temporal Dynamic Logic in PVS, Proceedings of the 29th International Conference on Types for Proofs and Programs TYPES 2023, 2023. Abstract.
• J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, and Lauren White, Towards an implementation of differential dynamic logic in PVS, Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), 2022.. BibTeX Reference.

The tag identifies links that are outside the NASA domain