The Logical Approach to Low-Level Stack Reasoning

—Formal verification of low-level programs often requires 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 previous work on stack typing. It is a variant of bunched logic and it 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. Keywords-program verification; separation logic; stack typing; hoare logic; frame rule

• Type: Conference
• Year: 2009
• Where: TASE
• Authors: Xinyu Jiang, Yu Guo, Yiyun Chen
• Keywords: Logic, Runtime Stacks, Separation Logic, Software Engineering, TASE 2009