Heute: 15.00 Uhr im Turing (00.09.055) Norbert Schirmer Statespaces --- The Locale Way Abstract: Verification of imperative programs is all about reasoning about the modifications of a program state. How should the state be represented in Isabelle/HOL? Some common approaches are discussed and a new flavour based on a distinctive feature of Isabelle, namely locales, is proposed. Norbert