DocumentCode
1399183
Title
The verification of low-level code
Author
Clutterbuck, D.L. ; Carré, B.A.
Author_Institution
Program Validation Ltd., Southampton, UK
Volume
3
Issue
3
fYear
1988
fDate
5/1/1988 12:00:00 AM
Firstpage
97
Lastpage
111
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;
fLanguage
English
Journal_Title
Software Engineering Journal
Publisher
iet
ISSN
0268-6961
Type
jour
Filename
6898
Link To Document