Keynote abstracts

Summary form only given. Despite their popularity and importance, pointer-based programs posed a major challenge for software verification. In this talk, we present a specification mechanism that is precise, concise and modular for automated verification of pointer-based programs. Our approach is built on top of separation logic that follows from pioneering works by Reynolds and O'Hearn. We focus on the development of a modular specification mechanism that can be used to provide both automated and scalable verification. Key features of our approach include the following. It can verify data structures with complex invariant properties. It provides a unified view of control flows that captures both multiple returns and exceptions. It can support more precise reasoning through structured specifications and path-sensitive error tracing. Last, but not least, we develop a way to decompose specifications into smaller fragments for more scalable verification. Our approach has been successfully applied to verify medium-sized programs from the imperative and object-oriented programming paradigms. Our verification methodology is being aimed at programs developed from mainstream programming languages.