The Logical Approach to Low-Level Stack Reasoning

Formal verification of low-level programs often require explicit reasoning and specification of runtime stacks. Treating stacks naively as parts of ordinary heaps can lead to very complex specifications and make proof construction more difficult. In this paper, we develop a new logic system based on the idea of memory adjacency from stack typing. It is a variant of bunched logic, and can be easily integrated into separation logic to reason about the interaction between stacks and heaps. Our logic is especially convenient for reasoning about stack operations, and it greatly simplifies both the specification and the proof of properties about stack-allocated data.