Programming and Verifying the Interactive Web

Server-side Web applications have grown increasingly common, sometimes even replacing brick and mortar as the principal interface of corporations. Correspondingly, Web browsers grow ever more powerful, empowering users to attach bookmarks, switch between pages, clone windows, and so forth. As a result, Web interactions are not straight-line dialogs but complex nets of interaction steps.

In practice, programmers are unaware of or are unable to handle these nets of interaction, making the Web interfaces of even major organizations buggy and thus unreliable. Even when programmers do address these constraints, the resulting programs have a seemingly mangled structure, making them difficult to develop and hard to maintain.

In this talk, I will describe these interactions and then show how programming language ideas can shed light on the resulting problems and present solutions at various levels. I will also describe some challenges these programs pose to computer-aided verification, and present solutions to these problems.