The logical approach to stack typing

We develop a logic for reasoning about adjacency and separation of memory blocks, as well as aliasing of pointers. We provide a memory model for our logic and present a sound set of natural deduction-style inference rules. We deploy the logic in a simple type system for a stack-based assembly language. The connectives for the logic provide a flexible yet concise mechanism for controlling allocation, deallocation and access to both heap-allocated and stack-allocated data. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages General Terms Reliability, Security, Languages, Verification Keywords stack, memory management, ordered logic, bunched logic, linear logic, type systems, typed assembly language

• Type: Conference
• Year: 2003
• Where: TLDI
• Authors: Amal J. Ahmed, David Walker
• Keywords: Assembly Language, Formal Methods, Logics, Programming Languages, TLDI 2003