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.

Wed 28 Oct

oopsla2015
10:30 - 12:00: OOPSLA - 1. Model Checking at Grand Station 1
Chair(s): Julian DolbyIBM Research
oopsla201510:30 - 10:52
Talk
Anthony Widjaja LinYale-NUS College, Singapore, Matthew HagueRoyal Holloway University of London, UK, C.-H. Luke OngUniversity of Oxford, UK
Link to publication
oopsla201510:52 - 11:15
Talk
Brian DemskyUniversity of California at Irvine, USA, Patrick LamUniversity of Waterloo, Canada
Link to publication
oopsla201511:15 - 11:37
Talk
Ivan KurajMassachusetts Institute of Technology, USA, Viktor KuncakEPFL, Switzerland, Daniel JacksonMassachusetts Institute of Technology, USA
DOI
oopsla201511:37 - 12:00
Talk
Casper Svenning JensenAarhus University, Denmark, Anders MøllerAarhus University, Veselin RaychevETH Zurich, Switzerland, Dimitar DimitrovETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
DOI