Automated Reasoning for Web Page Layout

Cassius automatically reasons about web pages. It formalizes a substantial fragment of CSS in an SMT-friendly way. Cassius can automatically verify, synthesize, and debug web pages.


Cassius supports the block, inline, floating, and positioned layout modes in CSS. It matches the behavior of existing web browsers and passes the official conformance tests.

(document A
   ([p] "Products:")
     ([div] "A")
     ([div] "B")
     ([div] "C")
     ([div] "D"))
   ([p] "Buy!"))))
(stylesheet B
 ((tag main)
  [width (% 100)]
  [float left])
 ((tag div)
  [width ?]
  [height (px 200)]
  [float left]))
(layout C
 ([ROOT :w 400]
      ([TEXT :w 112 :h 19])))
    ([BLOCK :w 400 :h 400]
     ([BLOCK] ([LINE] ([TEXT])))
     ([BLOCK] ([LINE] ([TEXT])))
     ([BLOCK] ([LINE] ([TEXT])))
     ([BLOCK] ([LINE] ([TEXT]))))
      ([TEXT :w 76 :h 10]))))))))
Cassius formalizes the relationship between HTML documents, CSS stylesheets, and rendered layouts, and can solve for unknowns.

Cassius can reason about all of these features quickly, frequently completing within minutes on small web pages.

The techniques that make Cassius possible are described in our OOPSLA'16 paper.

Cassius Project News

  1. Cassius has been accepted to OOPSLA'16. Read our paper to find out how Cassius works.
  2. Pavel Panchekha, the main author of Cassius, won the Adobe Research Fellowship for his work on Cassius.

The Cassius Developers

Cassius is developed by the University of Washington Programming Languages and Software Engineering group, by Pavel Panchekha and Emina Torlak.