K semantics for assembly languages: A case study

Citations of this article
Mendeley users who have this article in their library.


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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free