Jive Data and Store Model

Nicole Rauch 📧 and Norbert Schirmer

June 20, 2005

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This document presents the formalization of an object-oriented data and store model in Isabelle/HOL. This model is being used in the Java Interactive Verification Environment, Jive.


GNU Lesser General Public License (LGPL)


Session JiveDataStoreModel