We consider a specific kind of Abstract State Machines. It is shown how the machines can be used to provide a low-level formal semantics for a tiny object-oriented language, including control flow operators, object creation and field manipulation. Then the decidability result is established for checking invariants of programs corresponding to that class of ASMs.