Automated verification can ensure that a web page satisfies accessibility, usability, and design properties regardless of the end user's device, preferences, and assistive technologies. However, state-of-the-art verification tools for layout properties do not scale to large pages because they rely on whole-page analyses and must reason about the entire page using the complex semantics of the browser layout algorithm.
This paper introduces and formalizes modular layout proofs. A modular layout proof splits a monolithic verification problem into smaller verification problems, one for each component of a web page. Each component specification can use rely/guarantee-style preconditions to make it verifiable independently of the rest of the page and enabling reuse across multiple pages. Modular layout proofs scale verification to pages an order of magnitude larger than those supported by previous approaches.
We prototyped these techniques in a new proof assistant, Troika. In Troika, a proof author partitions a page into components and writes specifications for them. Troika then verifies the specifications, and uses those specifications to verify whole-page properties. Troika also enables the proof author to verify different component specifications with different verification tools, leveraging the strengths of each. In a case study, we use Troika to verify a large web page and demonstrate a speed-up of 13–1469x over existing tools, taking verification time from hours to seconds. We develop a systematic approach to writing Troika proofs and demonstrate it on 8 proofs of properties from prior work to show that modular layout proofs are short, easy to write, and provide benefits over existing tools.
Wed 23 OctDisplayed time zone: Beirut change
11:00 - 12:30
|Modular Verification of Heap Reachability Properties in Separation Logic|
OOPSLALink to publication DOI Pre-print File Attached
|Modular Verification of Web Page Layout|
Pavel Panchekha University of Utah, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle, Shoaib Kamil AdobeDOI
|Modular Verification for Almost-Sure Termination of Probabilistic Programs|
Mingzhang Huang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST AustriaDOI
|Leveraging Rust Types for Modular Specification and Verification|
Vytautas Astrauskas ETH Zurich, Switzerland, Peter Müller ETH Zurich, Federico Poli ETH Zurich, Switzerland, Alexander J. Summers ETH ZurichDOI Pre-print