Lightweight Separation

Abstract. Lightweight separation is a novel approach to automatic reasoning about memory updates in pointer programs. It replaces the spatial formulae of separation logic, which complicate automation, by independent assertions about the memory content and the memory layout. As a result, assertions about the content can be treated by existing reasoners. The effect of memory updates is evaluated using specialized tactics that prove disjointness of memory regions from a given memory layout.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Holger Gast
• Keywords: Artificial Intelligence, Memory Content, Memory Layout, Memory Updates, TPHOL 2008