Strachey Lecture - Formal methods reinvented - now with users, data, and inference

Formal methods reinvented - now with users, data, and inference 

I began my PhD by reading Scott and Strachey and taught denotational semantics to undergraduates, so Strachey influenced my career.    More recently, to my surprise, I have been thinking about the meanings of interactive software systems, and how users can contribute to what an application is. 

In this talk I will outline new analytics that help us understand user styles, redesign in the light of those styles, and evaluate the effects of redesign.  We do not assume tasks and there is no single generating process: users are heterogeneous and change style between and within each use.  We use the new analytics to infer admixture Markov models from user traces and then reason about the models with probabilistic temporal logic properties.  I will illustrate with a mobile app and a redesign, the app has over 35,000 users worldwide.  We have logged user traces of the original system and from after the redesign.  

This work is the result of collaboration over many years between designers, programmers, and formal analysts, involving research from HCI, inference, Markov models and probabilistic model checking.   It’s formal methods in the new millenium!

The lecture will be followed by refreshments in the Atrium. Doors open at 1.30 pm, please be seated by 1.50 pm.

The Strachey Lectures are generously supported by OxFORD Asset Management.