Mechanised Hypersafety Proofs about Structured Data
summary
Claims a practical verification path: LGTM encodes formats as getter code and proves correctness via parametrised hypersafety triples mechanised as a Coq embedding. Implementation is a C framework on CFML with domain tactics, and evaluation covers 13 case studies (sparse vectors/matrices, alpha blending). Proofs average 2.55× code length and reach up to 10× reduction versus unary approaches; rules, meta-theory, and soundness are fully mechanised and artifacts are available.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:25Verifying structured data
- 5:35Formats as code
- 8:00Hypersafety with getters
- 10:28Parametric triples
- 14:04Evaluation results
- 15:30Summary
- 15:52Q&A
related talks
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
01h 32mResearch Methods for Designing Next-Generation Programming Systems
01h 05mVerifying Infinitely Many Programs at Once
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
47mHow to trust a verified program?
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages