RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…)
summary
Claims a machine‑checked end‑to‑end proof that an interrupt‑free, fixed‑priority, non‑preemptive scheduler meets response‑time bounds by connecting program verification and response‑time analysis. Uses RefinedC for C trace invariants and Prosa extended with an overhead‑aware response‑time analysis, encodes timing via marker functions plus universally quantified timestamps, and verifies a C implementation Rössl (≈400 LOC) in Coq/RoCq/Iris. Proof and artifacts are fully formalized; no empirical tightness measurements yet.
AI-written summary · about
chapters (7)
- 0:00Refined Prosa intro
- 3:32Interrupt vs interrupt-free
- 6:23Refined Prosa approach
- 9:53Overheads in analysis
- 11:59Verifying Rossell with C
- 14:27Related work comparison
- 15:31Conclusion
related talks
19mFully Verified Instruction Scheduling
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
19mFormally Verified Superblock Scheduling
24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTL
15mClosing Remarks
09mBreaking the RISC-V Processor Customization Barrier with Formal Verification
56mProof Assistants At the Hardware-Software Interface
15mCompiling with Continuations, Correctly