Verification Support For Object Database Design

David Spelt

Research output: ThesisPhD Thesis - Research UT, graduation UT

62 Downloads (Pure)


In this thesis we have developed a verification theory and a tool for the automated analysis of assertions about object-oriented database schemas. The approach is inspired by the work of [SS89] in which a theorem prover is used to automate the verification of invariants for transactions on a relational database. The work presented in this thesis deals with an object-oriented database and it discusses applications other than the analysis of database transaction safety. An important difference with the work of [SS89] is that we have used a general purpose higher-order logic (HOL) theorem prover, namely the Isabelle theorem prover [Pau94, Isa], rather than implementing our own specialized prover. Much previous research, including the work of [SS89], concerns fully automatic techniques (i.e., without the possibility of further interaction). These techniques are inheritly limited in scope ([BGL96]). The presented approach, combines automatic and interactive proof, where Isabelle’s automatic proof facilities are exploited to minimize the user’s effort to discharge proof obligations. The results demonstrate that today’s prover technology can indeed help in practical verification issues that arise in the design of databases.
Original languageEnglish
Awarding Institution
  • University of Twente
  • Apers, P.M.G., Supervisor
  • Balsters, H., Co-Supervisor
Award date10 Sept 1999
Place of PublicationEnschede
Print ISBNs90-365135-53
Publication statusPublished - 10 Sept 1999


  • EWI-6360
  • IR-17908
  • METIS-118427


Dive into the research topics of 'Verification Support For Object Database Design'. Together they form a unique fingerprint.

Cite this