K Semantics for Assembly Languages: A Case Study

Formal verification of embedded software systems often requires a low-level representation of the program under scrutiny. It is often the case that the verification tools rely on ad-hoc encodings of particular assembly language semantics. In this paper we use the K framework to formally define a MIPS-based assembly language. Our proposed definition is modular in the sense that it accommodates various organizations for the storage-related aspects of the semantics. We also present how to instantiate our K language definition on two main memory models, corresponding to different representations of the assembly code. Such a formal language definition could be directly used by the program verification tools.