Decomposition of verification of machine programs based on control-state Abstract State Machines.
Werner Gabrisch · 2013
We are presenting a method verifying programs based on extended control-state Abstract State Machines (ASM). Programs are special initial states in ASM’s. The aim is to prove that every run holds an algebraic specification of functions. The proof of different functions could be made by independent steps. 1.