FMitF: Formal Verification of Accessibility

University Of Washington, Seattle WA

Investigators

Abstract

Most of the web is not designed for accessibility for the nearly one billion people that have a disability such as blindness, low vision, motorphysical impairments, or dyslexia, and no comprehensive, precise verification tools currently exist for checking accessibility. Existing testing tools are limited, imprecise, and incomplete, and even when they are used, they give guarantees only about one particular web browser configuration such as window size, default fonts and colors. This project aims to enable the formal verification of web accessibility. The research to be pursued involves the automatic identification of a broader class of accessibility problems that is currently possible and is intended to give guarantees of absence of such problems for all possible web browser configurations. The software tools developed in this project are intended to give web developers and content producers targeted, concrete feedback on who is affected by an accessibility issue, and why, and how to fix any problems. The project develops a user interface logic for specifying accessibility properties, and formalizes a large fragment of browser rendering algorithms using novel finitization reductions. The project builds software tools that translates web pages, accessibility rules, and the browser algorithm to quantifier-free linear real arithmetic, using an SMT solver to verify it or produce a concrete, inaccessible rendering of the webpage. To make the results of these verifications useful and usable to developers, content producers, and web users, the investigators develop new classes of concrete, comprehensible, and actionable warning explanations and new techniques for patching accessibility at run time. To evaluate all of this work, the project is partnering with Adobe, Instructure, and Wikimedia. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.