Procedure-Modular Verification of Control Flow Safety Properties


Soleimanifard, Siavash and Gurov, Dilian and Huisman, Marieke (2010) Procedure-Modular Verification of Control Flow Safety Properties. In: 12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010, June 22, 2010, Maribor, Slovenia. (In Press)

open access
Abstract: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
away completely. We evaluate the technique on a small but realistic case study.
Item Type:Conference or Workshop Item
Copyright:© 2010 ACM
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page