I provide two verification techniques for concurrent code. The first guarantees that values obtained from shared resources are of the expected type, and that accesses to shared resources will not deadlock. The second enforces access control on sequences of actions using policy automata. I also provide the first definition and proof of safe dynamic software update for behavioural properties of concurrent systems. I include techniques that reduce verification costs of behavioural properties and update safety.
|Published - 2011
|Grace Hopper Celebration of Women in Computing - Portland, Oregon, United States
Duration: 9 Nov 2011 → 12 Nov 2011
|Grace Hopper Celebration of Women in Computing
|9/11/11 → 12/11/11