Title :
The verification of low-level code
Author :
Clutterbuck, D.L. ; Carré, B.A.
Author_Institution :
Program Validation Ltd., Southampton, UK
fDate :
5/1/1988 12:00:00 AM
Abstract :
The formal verification of low-level code is a problem largely ignored by the academic community although it is seen as a major problem in industry. The paper examines the problems associated with verification at this level and describes SPADE-8080, a verifiable sublanguage of the Intel 8080. It also shows how programs written in SPADE-8080 can be analyzed and formally verified with the SPADE software tools
Keywords :
program verification; Intel 8080; SPADE-8080; low-level code; software tools; verification;
Journal_Title :
Software Engineering Journal
