Towards the verification of a generic interlocking logic: Dafny meets parameter...

on YouTube ↗20m

" summary

A generic interlocking logic is encoded in Dafny alongside the tool’s C/Python output, and a parameterized model checker is used to synthesize inductive invariants so Dafny can discharge safety proofs. A simplified case study with 5 components, 29 transitions and 18 variables proves two roots never occupy the same track section using Dafny code mirrors C/Python and parameterized model checker yields invariants. Current workflow is manual; goal is automated Dafny generation, automated model‑checker interaction and IDE integration.

AI-written summary · about

" chapters (16)

1. 0:00Interlocking logic in railways
2. 1:02Aida tool for design
3. 3:10Generating Dafny code
4. 5:58Dafny class structure
5. 8:07Formalizing specs in Dafny
6. 9:12Modeling scheduler for proofs
7. 10:37Early results and manual checks
8. 11:41Future automation and challenges
9. 12:06Q&A: Domain experts in proofs
10. 13:08Q&A: Fully automated verification
11. 14:13Q&A: Dafny vs Boogie/SMT
12. 15:18Q&A: Property spec logic
13. 16:22Q&A: Natural vs formal input
14. 17:27Q&A: Model checkers role
15. 18:56Q&A: Seagar loop automation
16. 20:00Closing remarks