Precise Reasoning about Container-Internal Pointers with Logical Pinning
Abstract
Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs.
Fields of Study & Subjects
Logic
programming
and type systems
Security and Verification in Computing
Distributed systems and fault tolerance
Publication details
- Pages
- 353–367
- Publication date
- 8 January 2026
- Language
- EN