A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures

Well-designed data structures are fundamental to the construction of robust programmes, particularly when their correctness can be established using formal methods. Currently, various successful deductive verification techniques exist but necessitate distinct and non-interoperable specifications and verification methods for data structure implementations. This paper presents a technique enabling cross-paradigm interoperable specification and verification of encapsulated data structures.

The novel approach builds on the shared mathematical foundations of algebraic data types (ADTs) across these diverse methodologies. The technique enables the coherent integration of components that have been verified using different deductive program verification approaches within a single project, provided that a regime of encapsulation is followed, which is slightly stricter than those imposed by the tools originally.

We formally introduce and discuss the encapsulation principle using a simplified conceptual object-oriented language and subsequently instantiate it for the Java programming language. This integration incorporates KeY, VeriFast, and Universe Types, thereby enabling heterogeneous verification projects in Java that encompass separation logic, dynamic frames, and ownership types.
... mehr

We demonstrate the applicability of our approach by conducting a cooperative verification of a client with three different data structures, of which each is verified with one of the aforementioned techniques.