On using VeriFast, VerCors, Plural, and KeY to check object usage

TL;DR

This paper evaluates four static verification tools for Java—VeriFast, VerCors, Plural, and KeY—in checking protocol compliance of shared, stateful objects using typestates, highlighting their strengths and limitations.

Contribution

It provides a comparative survey of four tools' effectiveness in verifying object protocols and analyzes the effort required to adapt code for verification.

Findings

VeriFast and VerCors effectively verify protocol compliance in shared objects.

Plural and KeY show limitations in handling aliasing and shared object protocols.

Programmer effort varies significantly across tools for achieving verification.

Abstract

Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state, in terms of a state machine. Usually, objects with protocol are either forced to be used in a linear way, which restricts what a programmer can do, or deductive verification is required to verify programs where these objects may be aliased. To evaluate the strengths and limitations of static verification tools for object-oriented languages in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader and of a linked-list, check for each tool its ability to statically guarantee protocol compliance as well as protocol completion, even when objects are shared in collections, and evaluate the programmer's effort in making the code acceptable to these tools.