Formal reasoning about runtime code update
Nathaniel Charlton, Ben Horsfall, Bernhard Reus · 2011
We show how dynamic software updates can be modelled using a “higher order store” programming language where procedures can be written to the heap. We then show how such updates can be proved correct with a Hoare-calculus that allows for keeping track of behavioural specifications of such stored procedures.