Login | Register

A modern Isabelle-based prover for VDM's logic of partial functions

Title:

A modern Isabelle-based prover for VDM's logic of partial functions

Karabotsos, George (2005) A modern Isabelle-based prover for VDM's logic of partial functions. Masters thesis, Concordia University.

[thumbnail of MR10289.pdf]
Preview
Text (application/pdf)
MR10289.pdf - Accepted Version
5MB

Abstract

Specification and verification tools, often, employ theorem proving technology. This technology encompasses an underlying logic encoded in a theorem prover. VDM-LPF, first developed by Sten Agerholm and Jacob Frost in 1996, encodes VDM's Logic of Partial Functions (LPF) by extending the generic theorem prover Isabelle. Because of Isabelle's powerful syntax facilities, terms in this logic are written using a subset of the VDM-SL specification language. In this thesis we provide the reader with a detailed description of the steps we undertake to revive the VDM-LPF logic by upgrading it to the latest Isabelle version, namely Isabelle2005, and by using its latest Intelligible Semi-Automated Reasoning (Isar) theory syntax. We first provide a description of the Isabelle theorem prover, its generic design, and the unique facilities it provides for extending itself and developing new object-logics. We then explain in detail the original VDM-LPF system as developed for the Isabelle94-8. We describe all the necessary modifications that were needed to perform the upgrade. Finally, a number of proofs are performed, using the upgraded VDM-LPF system, that form a case-study.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Karabotsos, George
Pagination:ix, 158 leaves ; 29 cm.
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science and Software Engineering
Date:2005
Thesis Supervisor(s):Chalin, Patrice
Identification Number:LE 3 C66C67M 2005 K37
ID Code:8505
Deposited By: Concordia University Library
Deposited On:18 Aug 2011 18:27
Last Modified:13 Jul 2020 20:04
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top