Structural Embeddings Revisited
summary
Formal verification shows the parallel-landing alert algorithm issues warnings for conflicts that occur between 9.5–10 seconds (a counterexample appears at 10.5s), using PVS proofs plus MuPAD visualization and an automated integration of MetiTarski to discharge 100 case splits. Work produces a deep interval-expression embedding and computational-reflection strategies, a floating-point embedding with the proof-producing tool Precisa, and a maintained NASA PVS library (53 developments, ~30k formulas) that supports these results.
AI-written summary · about
chapters (20)
- 0:00Intro
- 1:50Context
- 5:12Algorithm
- 6:38Verification
- 13:10Hybrid Verification
- 22:13Developing Libraries
- 25:38Evolving Libraries
- 30:07Verification Strategies
- 31:50High Level Structure
- 35:01Embeddings
- 35:54Interval Expressions
- 37:22Evaluation
- 38:16Theorems
- 40:40Status
- 41:02Structural embeddings
- 43:39Differential dynamic logic
- 46:05Floating point programs
- 46:33Golden age of embedding
- 48:02Recommendation
- 48:52Questions
related talks
29mA Temporal Differential Dynamic Logic Formal Embedding
41mLiving inside a Theorem Proving Universe
19mAn Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu...
01h 01mMulti-Modal Verification of Distributed Systems in Lean
46mRefinement Types from Light to Deep Verification
30mTrustworthy Formal Natural Language Specifications
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
53mSemantics-based program manipulation in the age of LLMs