When & Where: 12:00pm, Friday, September 26, 2008, Room 400 AKW
Abstract:
Despite their popularity and importance, pointer-based programs with linked data structures remain a major challenge for program verification. We design 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 we allow user-defined predicates to describe and formally reason with a wide-range of linked data structures.
To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. This procedure automatically infers the frame condition and translates its proof obligation for existing pure provers.
To improve expressivity, we support state-sets for proof search, multiple specs for methods and lemmas over related predicates. Recently, We have also applied it towards modular verification of OO programs. We have proven the soundness and termination of our verification system, and have built a working prototype system.
Some papers on our work can be found at: http://www.comp.nus.edu.sg/~chinwn