Automated Reasoning about Web Page Layout

Web pages define their appearance using Cascading Style Sheets. However, the CSS language is quirky and subtle, so it is difficult for designers to write, debug, and test their designs. Understanding all the ways a web page can be laid out, and ensuring that all these layouts are correct, is a persistent challenge.

In this talk, I'll describe how to formally verify that a web page layout is correct. To do so, correctness is first formalized in Visual Logic, a concise language for describing geometric properties of web page layouts. Visual Logic properties are true or false as a consequence of how a browser lays out a given page; we formalize a substantial fragment of browser layout in the Cassius framework. This formalization allows automated reasoning about CSS files. Building on that, the VizAssert tool automatically verifies layout properties expressed in Visual Logic, and the Troika proof assistant allows operating VizAssert in a modular fashion, decomposing a large web page into many components and verifying those components independently.

These tools demonstrate that formal verification has a bright future on the largest and most important application platform: the web.

Bio: Pavel Panchekha is an Assistant Professor in the School of Computing at the University of Utah, where he holds the Warnock Chair for Junior Faculty. He completed his PhD at the Paul G. Allen School for Computer Science and Engineering at the University of Washington, where he was advised by Michael D. Ernst and Zachary Tatlock. He has been awarded fellowships by the NSF, the ARCS foundation, Adobe Research, and the Wissner-Slivka foundation, and received his BS in mathematics from MIT. His research focuses on developing programming language techniques to meet challenges from all areas of computer science.