Automatic Verification of Conditions for Absence of Interrupts
Pavel Emeliyanenko
In order to the have possibility of verifying assembler programs written for the VAMP (Verified Architecture Microprocessor1) using the abstract software machine we need to relate the VAMP formal specification with the abstract software machine specification.
The software machine does not support interrupt handling and therefore programs to be executed on this machine should not produce any interrupts. In the previous work 11 the conditions for absence of interrupts were identified and their validity was proved using the PVS verification system. Besides that, a theorem was established which states that under certain conditions (including the conditions for absence of interrupts) the execution of a program on the software machine is equivalent to the execution of this program on the VAMP.
Consequently, if some property of a program has been proved using the software machine and the conditions stated in the theorem hold, then the same property holds during the execution of this program on the VAMP. The goal of this work is to develop software with help of which the required conditions for absence of interrupts can be proved automatically for most assembler programs.
Bachelor Thesis.