The Logical Approach to Low-level Stack Reasoning
(0) 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.
program verification separation logic stack typing hoare logic frame rule
Xinyu Jiang Yu Guo Yiyun Chen
Department of Computer Science and Technology University of Science and Technology of China Hefei, China The Software Security Lab, USTC Suzhou Institute of Advanced Study, USTC Suzhou, China
国际会议
天津
英文
209-216
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）