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)

Preview

PDF
242Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/72645
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page