Search NASA⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20220009052

Towards an Implementation of Differential Dynamic Logic in PVS

J. Tanner Slagel·César Muñoz·Swee Balachandran·Mariano Moscato·Aaron Dutle·Paolo Masci·Lauren White
View original source ↗Export metadata ↓

Abstract

The source did not provide an abstract. Follow the original record for more information.

Explore related subjects

Differential Dynamic LogicPrototype Verification SystemFormal VerificationFormal MethodsHybrid SystemsHybrid Programs

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, Lauren White. Towards an Implementation of Differential Dynamic Logic in PVS. https://ntrs.nasa.gov/citations/20220009052

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2022

Towards an Implementation of Differential Dynamic Logic in PVS

This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, which employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification process. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

Differential Dynamic Logic↗