- This event has passed.
Colloquium – Pavel Panchekha
February 14 @ 4:00 pm - 5:00 pm
University of Washington
February 14, 2019
lecture – 4:00pm
Host: Ganesh Gopalakrishnan
Automatically Verifying Web Page Layouts
Programming languages research develops techniques for reasoning about, debugging, and optimizing programs, especially in discrete, combinatorial domains. My work extends these techniques to new domains where traditional approaches have not been readily applicable, such as visual properties of web designs (OOPSLA’16, PLDI’18) or numerical methods for scientific computation (PLDI’15, PLDI’18, ICFP’18). This talk focuses on my recent work, establishing a foundation for formally verifying accessibility properties for web interfaces, and also briefly surveys the impact of my earlier research on automatically improving accuracy for numerical programs.
Ensuring that a web application is accessible to all users, across the diverse landscape of user configurations, is a challenge for today’s testing-based approach to layout debugging. My work on VizAssert demonstrates a fundamentally different approach: automatically proving a formal specification for a web page layout, across all user configurations. VizAssert implements a web browser in first order logic, allowing it to describe the possible renderings of the page as a set of logical equations, and solves these equations using an SMT solver to determine if it’s possible for a rendering to violate the specifications. VizAssert has verified hundreds of web page specifications, identified dozens of accessibility bugs, and provided feedback that enabled improving accessibility.
Like my work on web design, my earlier work on numerical accuracy developed new programming languages techniques to meet challenges from another domain. Developing reliable numerical software has traditionally been a tedious process requiring significant expertise. My work automates the process of finding an accurate way of evaluating a floating-point formula. My tool, Herbie, generates variants from an input formula using mathematical identities, evaluates those variants’ error using sampled inputs points, and selects the most accurate variant for each range of inputs. Herbie has proven effective in practice, recovering 70% of inaccurate bits on average and being used by scientists at NASA, Sandia, and NVIDIA.
Pavel Panchekha is a PhD candidate at the Paul G. Allen School for Computer Science and Engineering at the University of Washington, where he is 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. He has done eight hour cooking sessions, and is working on eight hour biking sessions.