Applying Formal Semantics of an Object-oriented Language to Program Invariant Checking

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.

• Type: Conference
• Year: 2005
• Where: ASM
• Authors: Andrey Novikov, Rostislav Yavorskiy
• Keywords: Abstract State Machines, ASM 2005, Low-level Formal Semantics, Microbiology, Tiny Object-oriented Language