Title: Automated reasoning about web page layout
Advisors: Michael Ernst and Zachary Tatlock
Supervisory Committee: Michael Ernst (Co-Chair), Zachary Tatlock (Co-Chair), Amy Ko (GSR, iSchool), Shoaib Kamil (Adobe Research), and James Fogarty
Abstract: Web pages are a common way for people to interact with applications critically important to their health, education, and livelihood. Web pages must correspondingly be accessible to all and easily usable. However, the technologies that web pages are developed in, chiefly HTML and CSS, are complex, with many unusual features and special cases. This talk discusses Cassius, a new attempt to make it easier to test and verify web page accessibility and usability. Cassius is a mathematical description of the web page layout algorithm used by web browsers, and an encoding of this specification to Satisfiability Modulo Theories, a format that allows efficient automated reasoning about web pages. Cassius has been used to build VizAssert, a tool to verify accessibility and usability assertions of a web page over all possible user configurations. The talk will discuss Cassius, VizAssert, and chart out ongoing work to make Cassius modular, allowing efficient reasoning about large web pages and web page components.