Formal reasoning about runtime code update
- Resource Type
- Conference
- Authors
- Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard
- Source
- 2011 IEEE 27th International Conference on Data Engineering Workshops Data Engineering Workshops (ICDEW), 2011 IEEE 27th International Conference on. :134-138 Apr, 2011
- Subject
- Computing and Processing
Communication, Networking and Broadcast Technologies
Servers
Runtime
Software
Semantics
Loading
Calculus
Computer crashes
- Language
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.