ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Hongseok Yang , Queen Mary, University of London
When:2009-12-13 09:00
Place:Room B103, Bldg 39, SNU


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.

Short bio


© Copyright 2008-2010 ROSAEC Center, Seoul National University