Wed 28 Oct 2015 10:30 - 10:52 at Grand Station 1 - 1. Model Checking Chair(s): Julian Dolby

HTML5 applications normally have a large set of CSS (Cascading Style Sheets) rules for data display. Each CSS rule consists of a node selector and a declaration block (which assigns values to selected nodes' display attributes). As web applications evolve, maintaining CSS files can easily become problematic. Some CSS rules will be replaced by new ones, but these obsolete (hence redundant) CSS rules often remain in the applications. Not only does this “bloat” the applications – increasing the bandwidth requirement – but it also significantly increases web browsers' processing time. Most works on detecting redundant CSS rules in HTML5 applications do not consider the dynamic behaviours of HTML5 (specified in JavaScript); in fact, the only proposed method that takes these into account is dynamic analysis, which cannot soundly prove redundancy of CSS rules. In this paper, we introduce an abstraction of HTML5 applications based on monotonic tree-rewriting and study its "redundancy problem". We establish the precise complexity of the problem and various subproblems of practical importance (ranging from P to EXP). In particular, our algorithm relies on an efficient reduction to an analysis of symbolic pushdown systems (for which highly optimised solvers are available), which yields a fast method for checking redundancy in practice. We implemented our algorithm and demonstrated its efficacy in detecting redundant CSS rules in HTML5 applications.

Conference Day
Wed 28 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:00
1. Model CheckingOOPSLA at Grand Station 1
Chair(s): Julian DolbyIBM Research
10:30
22m
Talk
Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting ApproachOOPSLA Artifact
OOPSLA
Anthony Widjaja LinYale-NUS College, Singapore, Matthew HagueRoyal Holloway University of London, UK, C.-H. Luke OngUniversity of Oxford, UK
Link to publication
10:52
22m
Talk
SATCheck: SAT-Directed Stateless Model Checking for SC and TSOOOPSLA Artifact
OOPSLA
Brian DemskyUniversity of California at Irvine, USA, Patrick LamUniversity of Waterloo, Canada
Link to publication
11:15
22m
Talk
Programming with Enumerable Sets of Structures
OOPSLA
Ivan KurajMassachusetts Institute of Technology, USA, Viktor KunčakEPFL, Switzerland, Daniel JacksonMassachusetts Institute of Technology, USA
DOI
11:37
22m
Talk
Stateless Model Checking of Event-Driven Applications
OOPSLA
Casper Svenning JensenAarhus University, Denmark, Anders MøllerAarhus University, Veselin RaychevETH Zurich, Switzerland, Dimitar DimitrovETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
DOI