In this paper we present our implementation of the Abstract State Machine(ASM) model, that has been defined in  to formalize the C# static and dynamic semantics. We show all the techniques we have used to get an efficient execution.
This work is part of a larger project which aims to establish some outstanding properties of C# and CLR virtual machine by mathematical proofs, such as the C# type safety and the correctness of the CLR bytecode verifier. As part of this
effort, an ASM model in form of an abstract interpreter has been developed in  for the full C# , including a thread and memory model . The implementation of the..