Code verification with the aid of MALPAS

The technique of static analysis has, for some time now, been recognised as a technique necessary for the verification of critical software. Typically static analysis is performed by the use of automatic tools. One such tool, widely used for the verification of safety critical software, particularly in the fields of military avionics and nuclear power, is MALPAS. The advantages of this particular tool are that, not only does it perform the simpler analyses of code structure and data and information flow, but it also reveals the semantics of the code under analysis which may be manually or automatically compared against specifications to verify the code