Procedure-Modular Verification of Control Flow Safety Properties

This paper describes a novel technique for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is achieved by relativizing the correctness of global properties on the local properties rather than on the implementations of methods, and is based on the construction of maximal models. Tool support is provided by means of ProMoVer, a tool that is essentially a wrapper around a previously developed tool set for compositional verification of control flow safety properties, where program data is abstracted a way completely. We evaluate the technique on a small but realistic case study.QC 2011082