Separation Logic from the Perspective of Program Analysis Seminars/Workshops

Abstract

The incorrect use of pointers, such as null pointer dereference and memory leak, is one of the most common sources of program errors. In this toturial, we will survey separation logic, an extension of Hoare logic that addresses this problem of pointers. This tutorial will focus on the application of the logic in program analysis, where remarkable progresses have been made in recent years. I will explain how proof rules of the logic formalize good programming idioms used by programmers, so as to support formal yet efficient verification of pointer programs, and how these rules have been exploited in the program analysis research to build efficient automatic program verifiers.