Web pages define their appearance using Cascading Style Sheets, a modular language for layout of tree-structured documents. In principle, using CSS is easy: the developer specifies declarative constraints on the layout of an HTML document (such as the positioning of nodes in the HTML tree), and the browser solves the constraints to produce a box-based rendering of that document. In practice, however, the subtleties of CSS semantics make it difficult to develop stylesheets that produce the intended layout across different user preferences and browser settings.
This paper presents the first mechanized formalization of a substantial fragment of the CSS semantics. This formalization is equipped with an efficient reduction to the theory of quantifier-free linear real arithmetic, enabling effective automated reasoning about CSS stylesheets and their behavior. We implement this reduction in Cassius, a solver-aided framework for building semantics-aware tools for CSS. To demonstrate the utility of Cassius, we prototype new tools for automated verification, debugging, and synthesis of CSS code. We show that these tools work on fragments of real-world websites, and that Cassius is a practical first step toward solver-aided programming for the web.
Wed 2 Nov Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 13:55 Talk | Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided Transformations OOPSLA Shachar ItzhakyMIT CSAIL, Rohit SinghMIT, Rezaul ChowdhuryStony Brook University, Kuat YessenovMIT, Yongquan LuMIT, Charles E. LeisersonMIT, Armando Solar-LezamaMIT CSAIL DOI Pre-print Media Attached | ||
13:55 - 14:20 Talk | Speeding Up Machine-Code Synthesis OOPSLA Venkatesh SrinivasanUniversity of Wisconsin - Madison, Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc. DOI Pre-print Media Attached | ||
14:20 - 14:45 Talk | Automated Reasoning for Web Page Layout OOPSLA DOI Media Attached | ||
14:45 - 15:10 Talk | FIDEX: Filtering Spreadsheet Data using Examples OOPSLA DOI Media Attached |