Benjamin Lerner

Modeling and Reasoning about DOM Events

copyright notice

Benjamin Lerner, Matt Carroll, Dan Kimmel, Hannah Quay-de la Vallee and Shriram Krishnamurthi


Web applications are fundamentally reactive. Code in a web page runs in reaction to events, which are triggered either by external stimuli or by other events. The DOM, which specifies these behaviors, is therefore central to the behavior of web applications. We define the first formal model of event behavior in the DOM, with high fidelity to the DOM specification. Our model is concise and executable, and can therefore be used for testing and verification. We have applied it in several settings: to establish some intended meta-properties of the DOM, as an oracle for testing the behavior of browsers (where it found real errors), to demonstrate unwanted interactions between extensions and validate corrections to them, and to examine the impact of a web sandbox. The model composes easily with models of other web components, as a step toward full formal modeling of the web.



download vcard icon
Email (essential):
Location (likely):
West Village H, Office 326
Post (possible):
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
work Lecturer Office 326