FMitF: Formal Verification of Accessibility

大多数网络并不是为近10亿残疾人（如失明、低视力、运动障碍或阅读障碍）设计的，目前还没有全面、精确的验证工具来检查无障碍性。现有的测试工具是有限的，不精确的，不完整的，即使使用它们，它们也只能保证一个特定的Web浏览器配置，如窗口大小，默认字体和颜色。本项目旨在实现对网页无障碍性的正式验证。将进行的研究涉及自动识别目前可能存在的更广泛的无障碍问题，目的是保证所有可能的网络浏览器配置都不存在此类问题。本项目开发的软件工具旨在为Web开发人员和内容制作者提供有针对性的具体反馈，说明谁受到了无障碍问题的影响，以及为什么以及如何解决任何问题。 该项目开发了一个用户界面的逻辑指定的可访问性属性，并正式使用新的有限化减少浏览器渲染算法的大片段。该项目构建了软件工具，将网页，可访问性规则和浏览器算法转换为无量化器的线性真实的算法，使用SMT求解器来验证它或生成网页的具体，不可访问的渲染。为了使这些验证的结果对开发人员、内容制作者和Web用户有用，研究人员开发了新的具体、可理解和可操作的警告解释类，以及在运行时修补可访问性的新技术。为了评估所有这些工作，该项目与Adobe、Instruct和Wikimedia合作。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

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.