Safety and Security
summary
A verified train controller models the full FRA kinematics in KeYmaera X, uses Taylor approximations, ghost differential equations and iterative bootstrapping, and cuts the literature controller’s conservative undershoot from over 2000 feet to 502 feet using over 180,000 proof steps (proof tactics ~2,545 lines; spec ~200 lines). Session also presents three concrete runtime-deviation algorithms (three algorithms) for deadline misses with Python/Julia implementations tested on an F1/10 steering model, a piecewise set-valued DNN abstraction with precision heatmaps for vision-based lane keeping, and NVM-assisted secure deletion that co-locates NVM+flash to improve deletion guarantees, performance and lifetime.
AI-written summary · about
chapters (12)
- 0:00Start
- 16:15Introduction
- 19:44Modeling deadline miss behavior
- 21:47Measuring deviation
- 23:30Uncertain Linear Systems approach
- 24:15Recurrence Relations approach
- 46:02State-of-the-art Secure Deletion For Flash memory
- 50:19Hybrid Evictor
- 51:57SHOCK Prefetching
- 52:34Experimental Setup
- 53:57Performance Testing
- 54:48Conclusion
related talks
21mAPP4MC RaceCar: A Practical ADAS Demonstrator for Evaluating and Verifying Timing Behavior
31mAutonomous driving, how Python drives Formula Racing cars
47mAchieving Software Quality Excellence Thru Software-Hardware Co-Design & Co-Verification
02h 25mEmbedded Systems Design
14mPANORover: Autonomous Driving System Development Platform
20mSLEIGHT: Real-time Closed-Loop Attack Analytics Framework for Holistic Intrusion...
19mBoosting confidence in tiny AI deployment in embedded control systems
31mMLOps for High-Stakes Environments