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. © 2014 Published by Elsevier B.V.
Asǎvoae, M. (2014). K semantics for assembly languages: A case study. In Electronic Notes in Theoretical Computer Science (Vol. 304, pp. 111–125). Elsevier. https://doi.org/10.1016/j.entcs.2014.05.006