Abstract Well-designed data structures are fundamental to the construction of robust programs, 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 originally imposed by the verification techniques. 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 integrates the approaches of KeY, VeriFast, and Universe Types, thereby enabling heterogeneous verification projects in Java that encompass Dynamic Frames, Separation Logic, and Ownership Types. We demonstrate the applicability of our approach by conducting a cooperative verification of a client with three different data structures, each of which is verified with one of the aforementioned techniques.

Abstract The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

One of the main factors of the increasing power of deductive verification tools are modern SMT solvers. Unfortunately, SMT solvers usually do not produce proof artifacts that could be inspected or checked. KeY is a formal platform for the deductive verification of Java programs which produces explicit, browsable proofs. SMT solvers can be driven from within KeY, but this unfortunately breaks these proof transparency intentions.