Regular Expression Analysis of Procedures and Exceptions,
Foster,J M · Defense Technical Information Center (DTIC) · 1985
This paper describes an algorithm used to find properties of computer programs by using algebraic methods. It is capable of handling subroutines and exception exits. A program scheme has been produced to implement it which is particularly aimed at finding properties of microcode programs. This scheme can be systematically instantiated to deal with particular properties. Great care has been taken with the efficiency of the algorithm; it works in practice, even for very complex microcode, in time proportional to the number of microcode instructions. Both the mathematical basis of the algorithm and the algorithm itself are explained. (Great Britain).