Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 11:22 - 11:45 at Olympia - Modular Verification Chair(s): Friedrich Steimann

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 Oct
Times are displayed in time zone: Beirut change

11:00 - 12:30: Modular VerificationOOPSLA at Olympia
Chair(s): Friedrich SteimannFernuni Hagen
11:00 - 11:22
Research paper
Modular Verification of Heap Reachability Properties in Separation Logic
OOPSLA
Link to publication DOI Pre-print File Attached
11:22 - 11:45
Talk
Modular Verification of Web Page Layout
OOPSLA
Pavel PanchekhaUniversity of Utah, Michael D. ErnstUniversity of Washington, USA, Zachary TatlockUniversity of Washington, Seattle, Shoaib KamilAdobe
DOI
11:45 - 12:07
Talk
Modular Verification for Almost-Sure Termination of Probabilistic Programs
OOPSLA
Mingzhang HuangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Amir Kafshdar GoharshadyIST Austria
DOI
12:07 - 12:30
Talk
Leveraging Rust Types for Modular Specification and Verification
OOPSLA
Vytautas AstrauskasETH Zurich, Switzerland, Peter MüllerETH Zurich, Federico PoliETH Zurich, Switzerland, Alexander J. SummersETH Zurich
DOI Pre-print