Archive

Despite their popularity and importance, pointer-based programs with linked data structures remain a major challenge for program verification. We propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach is based on separation logic and uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated properties.

To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. To improve expressivity, we support set of states for proof search, intersection types for methods and coercion rules for related shape predicates. Recently, We have also applied these modular and reusable verification techniques to OO programs. We have proven the soundness and termination of our verification system, and have built a working system.

©2007 Microsoft Corporation. All rights reserved.