An Evaluation of the ABEL System

Abstract

This thesis evaluates and discusses the ABEL system, an interactive theorem prover, developed at the Department of Informatics at the University of Oslo. The ABEL system is ultimately intended to be an environment for program development, including program verification, and is built on the work of Ole-Johan Dahl in the field of formal specification and verification.

A review of the necessary background theory is given, including short descriptions of some other theorem provers and verification systems. The review also includes explanations of the most prevalent techniques for mechanised theorem proving.

Additionally, the thesis contains a user's guide to the system, meant to help new users of the ABEL system getting started.

Some tests of the proof system is performed, wherein its performance with respect to the needs of program verification is investigated. An evaluation is performed, and conclusions drawn on what the system's main weaknesses are. Finally, with this evaluation as background, suggestions are made on how to develop the system further into a true verification system.