Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation
summary
A synchronous, stream-based language called MARVeLus combines Zelus-like discrete-time semantics with SMT-decidable refinement types to verify and then compile CPS code. The compiler uses a models keyword switch to verify against a physical model and then emit C-linked executables; verification generates VCs checked by Z3 and requires inductive invariants (follower decision and dynamics) for safety. A verified adaptive-cruise controller typechecks and then runs on an mBot mini (LiDAR, BeagleBone Blue), with simulation and real traces matching closely.
AI-written summary · about
chapters (14)
- 0:00Synchronous programming in robotics
- 1:24Synchronous programming for embedded
- 3:48Refinement types for verification
- 6:16Temporal properties in stream types
- 7:40Marvelous verification platform
- 9:26Adaptive cruise control safety
- 13:21Models versus real-world execution
- 17:15Autonomous braking system implementation
- 20:29Verification with SMT solvers
- 22:13Refinement type rules for streams
- 22:34Testing on mBot robot
- 23:57Comparison with verifiable CPS tools
- 26:05Summary and future work
- 27:49Q&A
related talks
15mAbstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
14mMultiparty Motion Coordination: From Choreographies to Robotics Programs
25mHigh-Level Mission Specification for Multiple Robots
21mProgramming-by-Demonstration for Long-Horizon Robot Tasks
20mAuthoring and Verifying Human-Robot Interactions
59mOn Human-robot Interactions via Multimodal Intent Modeling and Reachability-based Safety Assurance
15mKoord: A Language for Programming and Verifying Distributed Robotics Application
09mSituated Live Programming for Human-Robot Collaboration