Dynamic software updating
Elmo Todurov
Thursday, 28 February 2013, 14:00
Friday, 1 March 2013, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
G. Stoyle, M. Hicks, G. Bierman, P. Sewell, I. Neamtiu, Mutatis mutandis: safe and predictable dynamic software updating, TOPLAS 2007. doi: 10.1145/1255450.1255455
Abstract: This article presents a formal system for modelling dynamic upgrading of single-threaded programs. Programs are written in an imperative language with type aliases, global variables and functions, then translated to an annotated form where type casts from more abstract (more levels of type aliases) and more concrete (less levels) are explicit in code. When updating the application, the annotations make it easy to verify if an update is safe -- if the update changes type t, then t should not be used concretely in the remaining stack.
In the seminar, I plan to present an overview of the whole system, then translation into the annotated form, then operational semantics and the update process.
Tarmo Uustalu
Last update 27.2.2013