Verification of Templated Code in C++
summary
Claims a method to verify C++ templates without expanding the trusted computing base by treating unresolved symbols as hygienic macros and using a shallowly embedded logic. Uses Brick program logic with explicit substitutions and instantiation constraints to state specs over template bodies rather than instantiations, encodes evaluation order and implicit casts with predicate transformers/weakest preconditions, and shows mechanized proofs for several small function templates that discharge obligations and instantiate to concrete types.
AI-written summary · about
chapters (7)
- 0:00Templated code verification
- 1:44Template verification approach
- 3:50Specifying templated code
- 8:05Operator overloading and type resolution
- 10:16Predicate transformers for evaluation
- 11:20Conclusion and future work
- 11:43Q&A
related talks
01h 01mRethinking the Way We Do Templates in C++
59mHow and When To Write a C++ Template
27mCompositional Verification of Concurrent C Programs with Search Structure Templat...
21mMechanised Hypersafety Proofs about Structured Data
01h 01m“Mocking Frameworks considered harmful”
49mAre We Macro-free Yet?
19mPredictable Verification using Intrinsic Definitions
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)