Embedding differential dynamic logic in PVS

DOI10.4204/EPTCS.402.7MaRDI QIDQ6934135zbMATH OpenFDO

Authors J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César Muñoz, Swee Balachandran, Aaron Dutle

Publication date 3 September 2025

Full work available at URL https://doi.org/10.4204/EPTCS.402.7

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• A complete uniform substitution calculus for differential dynamic logic
• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• Affine arithmetic and applications to real-number proving
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Change and delay contracts for hybrid system component verification
• Differential dynamic logic for hybrid systems
• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• Differential game logic
• Differential Hybrid Games
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• dTL\(^{2}\): differential temporal dynamic logic with nested temporalities for hybrid systems
• Formal analysis of the compact position reporting algorithm
• Formal verification of Simulink/Stateflow diagrams
• Formalization of Bernstein polynomials and applications to global optimization
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• scientific article; zbMATH DE number 7699444 (Why is no real title available?)
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Logical foundations of cyber-physical systems
• MetiTarski: An automatic theorem prover for real-valued special functions
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Quantified Differential Dynamic Logic for Distributed Hybrid Systems
• Stochastic differential dynamic logic for stochastic hybrid programs
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Towards Self-verification of HOL Light
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Verifying hybrid systems with modal Kleene algebra
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system

This page was built for publication: Embedding differential dynamic logic in PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6934135)