An Overview of Separation Logic

After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of program verification for imperative programs using shared mutable data structures or sharedmemory concurrency.

• Type: Conference
• Year: 2005
• Where: VSTTE
• Authors: John C. Reynolds
• Keywords: Hoare Logic, Mutable Data Structures, Program Verification, Software Engineering, VSTTE 2005