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
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.
- 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.
identifies links that are outside
the NASA domain