This thesis evaluates and discusses the ABEL system, an interactivetheorem prover, developed at the Department of Informatics at theUniversity of Oslo. The ABEL system is ultimately intended to be anenvironment for program development, including program verification,and is built on the work of Ole-Johan Dahl in the field of formalspecification and verification.
A review of the necessary background theory is given, including shortdescriptions of some other theorem provers and verification systems.The review also includes explanations of the most prevalent techniquesfor mechanised theorem proving.
Additionally, the thesis contains a user's guide to the system, meantto help new users of the ABEL system getting started.
Some tests of the proof system is performed, wherein its performancewith respect to the needs of program verification is investigated. Anevaluation is performed, and conclusions drawn on what the system'smain weaknesses are. Finally, with this evaluation as background,suggestions are made on how to develop the system further into a trueverification system.