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.