A Correct-by-Construction Checker for Validation of Railway Data
summary
A correct-by-construction checker is formally specified and implemented in Why3, extracted to OCaml and linked with non-verified I/O to produce an executable that validates railway-network CSVs. The implementation uses a depth-first search on a graph that duplicates each segment into pre/next nodes to model forward-only train motion, with a proven equivalence to the original topology. The codebase is ~250 lines with ~150-line predicate defs, generates 182 verification conditions, plus a 59-VC reachability module and proofs of correctness; performance is competitive with existing tools.
AI-written summary · about
chapters (12)
- 0:00Railway data validation project
- 1:50Railway network properties
- 3:37Correct-by-construction checker in Y3
- 6:06Database constraints semantics
- 8:12Checker implementation and verification
- 9:16Network topology reachability
- 11:49Encoding networks for graph algorithms
- 13:37Reachability constraints verification
- 14:43Prototype results and optimizations
- 16:13Efficiency comparison with tools
- 17:48Graph algorithms for railways
- 19:13Conclusion
related talks
15mFormal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
18mSemantic-Type-Guided Bug Finding
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
15mCorrectness-by-Construction for Feature-Oriented Software Product Lines
21mMechanised Hypersafety Proofs about Structured Data
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
18mOn the Verification of a Subgraph Construction Algorithm