  Differential dynamic logic (dL) is a formal framework for specifying and
reasoning about hybrid systems, i.e., dynamical systems that exhibit both
continuous and discrete behaviors. These kinds of systems arise in many safety-
and mission-critical applications. This paper presents a formalization of dL in
the Prototype Verification System (PVS) that includes the semantics of hybrid
programs and dL's proof calculus. The formalization embeds dL into the PVS
logic, resulting in a version of dL whose proof calculus is not only formally
verified, but is also available for the verification of hybrid programs within
PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation
of dL for Hybrid Program Verification and Specification), supports standard dL
style proofs, but further leverages the capabilities of PVS to allow reasoning
about entire classes of hybrid programs. The embedding also allows the user to
import the well-established definitions and mathematical theories available in
PVS.
