TitleVerifying that web pages have accessible layout
Publication TypeConference Paper
Year of Publication2018
AuthorsPanchekha P, Geller A, Ernst MD, Tatlock Z, Kamil S
Conference NamePLDI 2018: Proceedings of the ACM SIGPLAN 2016 Conference on Programming Language Design and Implementation
Pagination1-14
Date or Month PublishedJune
Conference LocationPhiladelphia, PA, USA
AbstractUsability and accessibility guidelines aim to make graphical user interfaces accessible to all users, by, say, requiring that text is sufficiently large, interactive controls are visible, and heading size corresponds to importance. These guidelines must hold on the infinitely many possible renderings of a web page generated by differing screen sizes, fonts, and other user preferences. Today, these guidelines are tested by manual inspection of a few renderings, because 1) the guidelines are not expressed in a formal language, 2) the semantics of browser rendering are not well understood, and 3) no tools exist to check all possible renderings of a web page. VizAssert solves these problems. First, it introduces \emphvisual logic to precisely specify accessibility properties. Second, it formalizes a large fragment of the \emphbrowser rendering algorithm using novel \emphfinitization reductions. Third, it provides a \emphsound, automated tool for verifying assertions in visual logic. \par We encoded 14 assertions drawn from best-practice accessibility and mobile-usability guidelines in visual logic. VizAssert checked them on 62 professionally designed web pages. It found 64 distinct errors in the web pages, while reporting only 13 false positive warnings.
Downloadshttps://cassius.uwplse.org/ VizAssert and Cassius tools
Citation KeyPanchekhaGETK2018