The verification of low-level code
1988; Volume: 3; Issue: 3 Linguagem: Inglês
10.1049/sej.1988.0012
ISSN2053-910X
AutoresD.L. Clutterbuck, Bernard Carré,
Tópico(s)Embedded Systems Design Techniques
ResumoThe 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. This paper examines the problems associated with verification at this level and describes SPADE-8080, a verifiable sub-language of the Intel 8080. It also shows how programs written in SPADE-8080 can be analysed and formally verified with the SPADE software tools.
Referência(s)