Reachability Analysis of the HTML5 Parser
Specification and its Application toCompatibility Testing
Yasuhiko Minamide and Shunsuke Mori
University of Tsukuba, Japan

Abstract. A draft standard for HTML, HTML5, includes the detailed
specification of the parsing algorithm for HTML5 documents, including error handling. In this paper, we develop a reachability analyzer forthe parsing specification of HTML5 and automatically generate HTML
documents to test compatibilities of Web browsers. The set of HTML
documents are extracted using our reachability analysis of the statements in the specification. This analysis is based on a translation of thespecification to a conditional pushdown system and on a new algorithm
for the reachability analysis of conditional pushdown systems.
In our preliminary experiments, we generated 353 HTML documents
automatically from a subset of the specification and found several compatibility problems by supplying them to Web browsers.

1

Introduction

A draft standard for HTML, HTML5 [Con12], includes the detailed specification of the parsing algorithm for HTML5 documents, including error handling.
Although it is intended that this will solve compatibility issues in HTML parsing, several current implementations of Web browsers and parsing libraries havecompatibility issues caused by the complexity of the specification.
In this paper, we develop an analyzer for the specification that checks thereachability of statements in the specification. We then apply the analyzer togenerate a set of HTML documents automatically, which are used to test compatibilities of Web browsers with respect to the specification. The set of generated
HTML documents enables path testing. That is, the tests cover both true andfalse cases for all conditional statements in the specification. The reachability
analysis is based on a translation of the specification to a conditional pushdown
system [LO10] and on a new algorithm for the reachability analysis of conditional
pushdown systems.
In the first step of the development, we introduce a specification language todescribe the parsing algorithm of HTML5 formally. We concentrate on the stageof parsing that follows tokenization, called tree construction in the specification.
The algorithm for the tree-construction stage is specified in terms of a stackmachine, with the behaviour for each input token being described informallyin English. We formalize the specification by introducing an imperative programming language with commands for manipulating the stack. The distinctive
feature of the specification is that the specification inspects not only the top of
the stack, but also the contents of the whole stack. Furthermore, the parsing algorithm destructively modifies the stack for elements called formatting elements.
However, we exclude formatting elements from our formalized specification because of difficulties with the destructive manipulation of the stack. This is themain limitation of our work.
Our reachability analysis of the specification is based on that for conditional
pushdown systems. Esparza et al. introduced pushdown systems with checkpoints that has the ability to inspect the contents of the whole stack and showedthat they can be translated to ordinary pushdown systems [EKS03]. Li andOgawa reformulated their definition and called them conditional pushdown systems [LO10]. The translation to ordinary pushdown systems causes the size ofthe stack alphabet to increase exponentially, which makes direct translation infeasible for the implementation of the reachability analysis. To overcome thisproblem, we design a new algorithm for reachability analysis that is a direct extension of that for ordinary pushdown systems [BEM97,EHRS00]. Our algorithm
is obtained by extending P-automata that describe a set of configurations to automata with regular lookahead. Although it still has an exponential complexity,
it avoids the exponential blowup caused by the translation before applying thereachability analysis.
We have developed a reachability analyzer for the HTML5 parser specification based on the translation to a conditional pushdown system and on thereachability analysis on it. A nontrivial subset of the tree-construction stage consisting of 24 elements and 9 modes is formalized in our specification language.
In our preliminary experiments, we have generated 353 HTML documents automatically from the subset of the specification and found several compatibility
problems by supplying them to Web browsers.
This paper is organized as follows. Section 2 reviews the HTML5 parser
specification and introduces our language for formalizing the specification. The
reachability analysis of the specification and its application to test-case generation are also discussed in this section. We introduce conditional pushdown
systems and present a new algorithm for their reachability analysis in Section 3.
The translation from the specification language to conditional pushdown systems is described in Section 4. In Section 5, we describe our implementation andpresent our experimental results. Finally, we discuss related work and conclude.

2

HTML5 Parser Specification and Reachability Analysis

2.1

HTML5 Parser Specification

The algorithm for the HTML5 parsing is specified as a stack machine whose
behaviour depends on a variable called the insertion mode. The insertion mode
keeps track of the part of an HTML document that the parser is processing, suchas “initial”, “in body”, or “in table”. The stack of open elements stores elementsthat have not yet been closed during parsing, and is used to match corresponding
end tags and to handle errors. When the parser inserts a new HTML element,
it appends the new element to the top element of the stack and pushes it onto
the stack as follows.
P
HEAD

BODY

HEAD
BODY

P

BODY

insert “p”

BODY

HTML

HTML

HTML

HTML

DOM TreeStack

DOM TreeStack

The specification is written in English and is quite complex. The following ispart of the HTML5 specification for the “in body” insertion mode.
,→ A start tag whose tag name is one of: ..., “p”, ...
If the stack of open elements has a p element in button scope,then act as if an end tag with the tag name “p” had been seen.
Insert an HTML element for the token.
The specification is sometimes rather difficult to interpret precisely, and it is notpossible to analyze the specification mechanically.
The first step in the analysis of the specification is to introduce a specification
language. Figure 1 is an example of a formalized specification using our specification language. The specification comprises a set of mode definitions, with eachmode definition containing specifications of the behaviour for start and end tagsin the mode. The behaviour for each tag is described as an imperative programthat manipulates the stack of open elements with commands including PUSH andPOP. We also allow the following commands:– MODE[mode] changes the insert mode to mode. The change of mode affects
the behaviour of the PSEUDO command below.
– PSEUDO[t] is basically a procedure call and the parser acts as if a tag t had
been seen.
– ERROR records that an error is encoutered during parsing and does nothingin our model.
In the specification for each tag, the variable me refers to the element name forthe tag. The command insertElement is currently defined as follows.
sub insertElement [target] = PUSH [target]

This definition is used because we are currently interested only in the reachability
analysis of the specification and are ignoring the construction of the DOM tree.
The most notable feature of the specification language is the inspection of
the current stack content. In the example, the current contents of the stackmode inbody{<p> : {
if isInScope[ buttonScopeElements, {P} ] then
PSEUDO[</p>];insertElement[me]}<h1>, <h2> : {...
if match[ {H1 | H2} .* ] then{
ERROR; POP};insertElement[me]}<table> : {insertElement[{Table}];MODE["intable"]}...
}Fig. 1. Example of a formalized specification
The stack of open elements is said to have an element in a specific scope consisting ofa list of element types list when the following algorithm terminates in a match state:
1. Initialize node to be the current node (the bottommost node of the stack).
2. If node is the target node, terminate in a match state.
3. Otherwise, if node is one of the element types in list, terminate in a failure state.
4. Otherwise, set node to the previous entry in the stack of open elements and returnto step 2. (This will never fail, since the loop will always terminate in the previous
step if the top of the stack — an html element — is reached.)
Fig. 2. The algorithm of “have a element in a specific scope”

are inspected by a regular expression match[ {H1 | H2} .* ], where regularexpression {H1 | H2} .* represents stacks whose top element is either H1 or H2.
The real capability stack inspection is utilized in the definition for <p> as
isInScope[ buttonScopeElements, {P} ]. It is the formalization of “have anelement in a specific scope” and its specification is shown in Figure 2. Although
the algorithm is rather complicated, the property can be checked by the following
inspection of the stack using a regular expression:
fun isInScope [list,target] = match[ (element \ list)* target .* ]where element is a variable representing the set of all elements, and therefore
the set element \ list contains elements that exclude those in list.
In the formalization of the HTML5 specification, we also make explicit someof the implicit assumptions that appear in the specification. In the following

mode inbody {<select> : { PUSH[ me ]; MODE["inselect"] }}mode inselect {<option>, <optgroup> : { PUSH[ me ] }</optgroup> : {if match[ {Option} {Optgroup} .* ] thenPOP// (A)else
NOP;// (B)
if match[ me .* ] thenPOP// (C)else
ERROR // (D)}}Fig. 3. Example for reachability analysis

example, it is assumed that, at this point, the stack of open elements will have
either a “td” or “tr” element in the table scope.
If the stack of open elements has a td element in table scope, then act as
if an end tag token with the tag name ”td” had been seen.
Otherwise, the stack of open elements will have a th element in table
scope; act as if an end tag token with the tag name ”th” had been seen.
We formalize this specification by using the command FATAL and show that
FATAL is not reachable by applying our reachability analyzer. Please note that
it is normal to reach an ERROR command because it just records the parser
encounter an ill-formed HTML document.
if isInTableScope [ { Td } ] then ...
else if isInTableScope [ { Th } ] then ...
else FATAL

2.2

Reachability Analysis and Test Generation

We analyze the reachability of specification points via translation to a conditional pushdown system. The main application is to test the compatibility of
HTML5 parsing with Web browsers and parsing libraries. Our reachability analyzer generates test cases that cover both true and false cases for all conditional
statements in the specification.
Let us consider the example shown in Figure 3. To cover both true andfalse cases for all conditional statements, our reachability analyzer must checkthe reachability of the points (A)–(D). By translating the specification to aconditional pushdown system and applying the reachability analysis describedin Section 3.2, the analyzer finds that the point (A) is reachable from the initialstate of inbody with the empty stack by the following input.

<select><optgroup><option></optgroup>

A test document is generated from this input by appending appropriate end
tags as follows. By executing the interpreter of the specification language, we
compute the stack after the execution for the above input. Before the executionof (A), we have stack Option, Optgroup, Select. The pop statements at (A)and (C) are then executed. The execution for the input then results in stack
Select. We therefore generate the following HTML document as a test case by
appending the end tag of Select.
<select><optgroup><option></optgroup></select>

By applying the same method, we obtain the following test cases for (B)–(D).
<select></optgroup></select>// (B)<select><optgroup></optgroup></select> // (C)<select></optgroup></select>// (D)

We can then test the compatibility of Web browsers by supplying test cases
generated in this manner as HTML documents.

3

Conditional Pushdown Systems and Reachability
Analysis

We translate our specification language into conditional pushdown systems of
Li and Ogawa [LO10], which are a reformulation of pushdown systems withcheckpoints [EKS03]. Conditional pushdown systems extend ordinary pushdown
systems with the ability to check the contents of the whole stack against a regular
language.
3.1

Regular Languages and Derivatives

We briefly review the theory of regular languages with a focus on the derivatives of regular languages [Brz64]. The theory of derivatives has drawn renewed
attention as an implementation technique for parsing and decision procedureson regular languages [ORT09,KN11]. Let Reg(Γ ) be the set of regular languages
over Γ .
For L ⊆ Γ ∗ and w ∈ Γ ∗ , the derivative 1 of L with respect to w is written as
w−1 L and defined as follows.
w−1 L = {w0 | ww0 ∈ L}
Brzozowski showed that there are a finite number of types of derivatives foreach regular language. More precisely, the set {w−1 L | w ∈ Γ ∗ } is finite forany regular language L over Γ . This fact is the key to the termination of ouralgorithm for the reachability analysis of conditional pushdown systems.
1

The derivative w−1 L is also called the left quotient in many litterateurs.

In this paper, regular languages are often described in terms of regular expressions. The syntax of regular expressions over Γ is defined as follows2 :R ::= ∅ |  | γ | R · R | R + R | R∗
where γ ∈ Γ . We write L(R) for the language of regular expression R. We saythat a regular expression R is nullable if  ∈ L(R). We characterize nullable
expressions in terms of following function ν(R).
ν(∅) = ∅ν(γ) = ∅ν(R1 + R2 ) = ν(R1 ) + ν(R2 )ν() = ν(R∗ ) = ν(R1 · R2 ) = ν(R1 ) · ν(R2 )Brzozowski showed that the derivative γ −1 R of a regular expression can becomputed symbolically using ν(R), as follows:
γ −1 ∅ = ∅γ −1 γ = −1 ∗γ R = (γ −1 R)R∗

γ −1  = ∅γ −1 γ 0 = ∅−1
γ (R1 + R2 ) = γ −1 R1 + γ −1 R2

γ −1 R1 · R2 = (γ −1 R1 )R2 + ν(R1 )(γ −1 R2 )The derivative of a regular expression can be extended for words with −1 R = R
and (γw)−1 R = w−1 (γ −1 R). We then have w−1 L(R) = L(w−1 R).
Our implementation utilizes regular expressions extended with intersection
and complement. The derivatives of extended regular expressions are computed
similarly, as described in [ORT09]. The automaton corresponding to a regularexpression is constructed only when we decide the language inclusion between
two regular expressions.
3.2

Conditional Pushdown Systems

We now review conditional pushdown systems that have the ability to checkthe current stack contents against a regular language, and then present a newalgorithm for the reachability analysis.
Definition 1. A conditional pushdown system P is a structure hP, Γ, ∆i, where
P is a finite set of states, Γ is a stack alphabet, and ∆ ⊆ P ×Γ ×P ×Γ ∗ ×Reg(Γ )is a set of transitions.
A configuration of conditional pushdown system P is a pair hp, wi wherep ∈ P and w ∈ Γ ∗ . The set of all configurations is denoted by C. We writeR

hp, γi ,→ hp0 , wi if hp, γ, p0 , w, Ri ∈ ∆. The reachability relation is defined as
an extension of that for ordinary pushdown systems. A configuration hp, γw0 i
Ris an immediate predecessor of hp0 , ww0 i if hp, γi ,→ hp0 , wi and w0 ∈ R: the2

For regular expressions in our specification language, we write alternation as R1 |R2instead of R1 + R2 .

regular language R inspects the current stack contents excluding its top. The
reachability relation =⇒ is the reflexive and transitive closure of the immediate
successor relation. Then, the predecessor function pre∗ : 2C → 2C is defined bypre∗ (C) = {c | ∃c0 ∈ C.c =⇒ c0 }.
Let us consider the following conditional pushdown system P1 shown below.
R

A transition labeled with γ/w|R from p to p0 denotes transition rule hp, γi ,→hp0 , wi, and a transition labeled with γ/w is an abbreviation of γ/w|Γ ∗ .
a/aa, a/ca
a/ba, b/ab
c/cc, c/ac
b/|abΓ ∗
a/

p0

a/ba

p1

a/

p2

a/a|a∗ ccΓ ∗In the transition from p0 to p2 , the condition a∗ ccΓ ∗ is used to check that two
c’s were pushed at p0 consecutively. In the transition from p1 to p1 , the conditionabΓ ∗ is used to prevent the popping of the last b on the stack.
As discussed by Esparz et al. [EKS03], a conditional pushdown system can betranslated into an ordinary pushdown system by expanding its stack alphabet.
However, the translation causes the size of the stack alphabet and the transition relation to grow exponentially, and it is therefore not feasible to apply thetranslation for the reachability analysis directly.
3.3

New Algorithm for Reachability Analysis

We describe our new algorithm for the reachability analysis of conditional pushdown systems. The reachability analysis of ordinary pushdown systems represents a regular set of configurations with P-automata [BEM97,EHRS00]. We
directly extend the algorithm by representing a regular set of configurations
with P-automata using regular lookahead.
Given a conditional pushdown system P = hP, Γ, ∆i, a P-automaton uses P
as a set of initial states and Γ as the input alphabet.
Definition 2. A P-automaton with regular lookahead is a structure A = hΓ, Q, δ,
P, F i, where Q is a finite set of states satisfying P ⊆ Q, δ ⊆ Q × Γ × Q × Reg(Γ )is a set of transition rules, and F is a set of final states.
w|w0

We introduce the transition relation of the form q −→ q for P-automata withregular lookahead: it means that, at the state q, the automaton may consume w
and change its state to q 0 if the rest of the input is w0 . This is defined as follows:
|w– q −→ q for any q ∈ Q and any w ∈ Γ ∗ ,γ|w– q −→ q 0 if hq, γ, q 0 , Ri ∈ δ and w ∈ R,
wγ|w0

w|γw0

γ|w0

– q −→ q 0 if q −→ q 00 and q 00 −→ q 0 .

Then, the set of configurations represented by A is defined as Conf(A) = {hp, wi |w|p ∈ P and p −→ q for some q ∈ F }.
To formulate our new algorithm for reachability analysis, we also extend the
w|Rtransition rules to those involving many steps, namely q −−* q 0 , as follows:
|Γ ∗

– q−
−* q,
γ|R

– q−
−* q 0 if hq, γ, q 0 , Ri ∈ δ,
– qwγ|γ −1 R1 ∩R2

−
−*

w|R1

γ|R2

q 0 if q −−* q 00 and q 00 −−* q 0 .

In the third case of the above definition, the two transition rules are combinedby composing two lookahead sets via quotient and intersection: γ −1 R1 ∩ R2 . At
the state q 0 , γ −1 R1 must be satisfied because the symbol γ is consumed by thetransition from q 00 to q 0 . The following lemma relates the extended transition
rules to transitions.
Lemma 1.
w|R

w|w0

– If q −−* q 0 and w0 ∈ R, then q −→ q 0 .
w|R

w|w0

– If q −→ q 0 , then q −−* q 0 and w0 ∈ R for some R.
The P-automaton Apre∗ representing pre∗ (Conf(A)) can be computed byextending the saturation rule of [BEM97]. That is, Apre∗ is obtained by adding
new transitions according to the following extended saturation rule:
w|R2

R1

−* q in the current automaton, add a transition– If hp, γi ,→ hp0 , wi and p0 −rule pγ|R1 ∩R2−−*

q.

Based on this saturation rule, we have also extended the efficient algorithm forthe reachability analysis [EHRS00] in a straightforward manner.
The following lemma and the finiteness of derivatives of a regular language
guarantee the termination of the application of the saturation rule.
Lemma 2. Let R = {R | hq, γ, q 0 , Ri ∈ δ for some q, γ, q 0 }.
w|RT
If q −−* q 00 , then R = R0 for some R0 ⊆ {w−1 R | R ∈ R ∧ w ∈ Γ ∗ }.
Let us consider the previous conditional pushdown system P1 . We apply thesaturation algorithm to P1 to check the reachability to the set of configurations
C1 = {hp2 , wi | w ∈ L(c(a + c)∗ bΓ ∗ )}. The P1 -automaton in Figure 4 excluding
the dashed transitions represents C1 by using lookahead. The dashed transitions
are added by applying the saturation rule. The three transitions from p0 to qf
are added from the top. This shows that the configuration C1 is reachable fromp0 with a stack satisfying (a + c)+ bΓ ∗ .

a|a∗ ccΓ ∗a|bΓ ∗

p0

p1

a
a

p2
c|(a + c)∗ bΓ ∗b|abΓ ∗
qfa|cΓ ∗ ∩ (a + c)∗ bΓ ∗c|(a + c)∗ bΓ ∗a|(a + c)∗ bΓ ∗a, b, cFig. 4. P1 -automaton obtained by the saturation algorithm

4Translation to Conditional Pushdown Systems

In this section, we present the translation of the specification language to conditional pushdown systems.
4.1

Expanding Pseudo Statements

The first step of the translation is to expand pseudo statements PSEUDO[t] at
non-tail positions. This is necessary because PSEUDO[t] is basically a procedure
call and its simulation requires another stack that is not synchronized with thestack of open elements. Pseudo inputs at tail positions can be translated directly
into transitions of a pushdown automaton. To avoid infinite chains of inline
expansion, we do not expand PSEUDO[t] inside the code for the tag t. In thefollowing example, PSEUDO[</p>] in <p> and PSEUDO[<p>] in </p> should be
expanded because they are not at tail positions.
<p> : {
if isInButtonScope[ {P} ] then
PSEUDO[</p>];insertElement[me]}</p> : {if !isInButtonScope [ {P} ] then {PSEUDO[<p>]; PSEUDO[</p>]} else {popuntil[{P}]}}We obtain the following code by expanding them. Because we cannot expand
PSEUDO[<p>] in the code for <p>, it is translated into FATAL. If the FATAL introduced in this translation is reachable, then the translation will not be faithful.
However, this is not the case in this example because PSEUDO[<p>] is constrainedby isInButtonScope[ {P} ] and !isInButtonScope[ {P} ].

<p> : {if isInButtonScope[ {P} ] then {if !isInButtonScope [ {P} ] then {PSEUDO[<p>]; => FATALPSEUDO[</p>]} else {popuntil[{P}]}}insertElement[me]}...

In order to check that FATAL statements introduced by this expansion are
not reachable, we check their reachability after the translation to a conditional
pushdown system. For the subset of the HTML5 specification we have formalized,
our reachability analyzer showed that they are not reachable.
4.2

Translation to Conditional Pushdown Systems

After expansion of pseudo statements, a specification is translated to a conditional pushdown automaton. Then, a conditional pushdown system is obtainedby forgetting the input of the pushdown automaton. Let us consider the following
specification as an example.
</p> : {if match[ {Li}*{P}.* ] then {while !match[{P} .*] do POP; POP}}<p> : { PUSH[{P}] }This can be converted into the following state transition diagram, where eachtransition is labeled with a tag indicating input, push, pop, or the condition
under which the transition occurs.
<p>

</p>

¬P.∗
∗

Li P.

∗

¬Li∗ P.∗pop

push Ppop

P.

∗

The transitions labeled with a tag, push, or pop can be translated directly tothose of pushdown automata. The transition label with a regular expression
representing the condition under which it occurs is translated as follows. Let us
consider a transition labeled with a regular expression R from q to q 0 .
γ −1 R– For each γ in the stack alphabet, a transition hq, γi ,→ hq 0 , γi is added tothe pushdown automaton.

In this example, the previous state transition diagram is translated to thefollowing conditional pushdown automaton under the stack alphabet {P, Li}:
<p>

</p>

Li/Li | .∗Li/Li | Li∗ P.∗
P/P | .∗

Li/Li | ¬Li∗ P.∗
pop

push P
pop

P/P | .

∗

where push and pop are not translated for simplicity. The following derivatives
are used in the translation.
Li−1 (Li∗ P.∗ ) = (Li−1 (Li∗ ))P.∗ + ν(Li∗ )Li−1 (P.∗ ) = Li∗ P.∗
P−1 (Li∗ P.∗ ) = (P−1 (Li∗ ))P.∗ + ν(Li∗ )P−1 (P.∗ ) = .∗5

Experimental Results

We have implemented the reachability analyzer of our specification language. It
performs the translation from the specification language to conditional pushdown
systems and reachability analyses for these systems. It is implemented in OCaml
and based on the library for automata used in the PHP string analyzer [Min05].
The main application of the analyzer is to generate automatically a set ofHTML test documents from a specification. It is also used to check the consistency of the specification and the translation. The current implementation
checks for consistency in the following two respects.
– The execution of the specification cannot cause stack underflow.
– FATAL statements in the specification or introduced by the translation are
unreachable.
The analyzer showed that these properties hold for the subset of the HTML5
parser specification described below.
We have formalized a nontrivial subset of the tree-construction stage of the
HTML5 specification. It is 438 lines in length, excluding comments and empty
lines, and contains the specification of 24 elements and 9 modes. This specification can be obtained from http://www.score.cs.tsukuba.ac.jp/~minamide/
html5spec/model.html5. As we mentioned in the Introduction, this subset excludes the specification of formatting elements, which is one of the main limitations of our work to date.
We applied our reachability analyzer to the specification using a Linux PC
with an Intel Xeon processor (3.0 GHz) and 16 GB memory. The specificationis translated to a conditional pushdown automaton with 487 states, and there
are 1186 specification points3 whose reachability had to be checked. For thesepoints, our reachability analyzer showed that 828 points were reachable from the3

In the implementation, a specification point is represented by a pair comprising astate and a regular expression. We may therefore have more specification points thanstates.

initial state and generated 353 HTML documents excluding duplicates. In thefollowing table, the first row shows the length of an input sequence of tags andthe second row shows the number of points. For example, there are 380 points
for which the analyzer found an input sequence of length 3.
Length 1# Points 46

2
3
4
167 380 198

5
35

6
2

The reachability of the specification points was checked by applying the algorithm described in Section 3.2 by adding the final states corresponding to themin the P-automaton. It took 82 minutes to check the reachability of all the points
and required more than 3 Gbyte of memory during the computation.
We conducted compatibility tests on the following Web browsers and HTML5
parser libraries: html5lib [htm] is implemented in Python and closely follows the
specification, and htmlparser, the Validator.nu HTML parser [Val], is implemented in Java and has been used for HTML5 in the W3C markup validation
service. The experiment was conducted on Mac OS X, version 10.7.3. The following table shows the number of incompatibilities found when using the generated
set of 353 HTML documents. The numbers in parentheses are obtained after
merging similar incompatibilities.4
Safari Firefox Opera
IE 5 html5lib htmlparser
Version
5.1.3
10.0.1
11.61
0.95
1.3.1
# Incompatibilities
1
6
0
0
3
6
(1)
(2)
(1)
(2)
The three main incompatibilities found in this experiment are listed below.
The lines labeled ‘Test’ and ‘Spec’ are the HTML documents generated by our
analyzer and the serialized representation of the results of parsing with the
HTML5 specification, respectively. The incompatible results are shown following
the Spec lines.
Test : <body><dd><optgroup><dd></dd></body>Spec : <body><dd><optgroup></optgroup></dd><dd></dd></body>
Safari, Opera, html5lib, IE: <body><dd><optgroup><dd></dd></optgroup></dd></body>Firefox, htmlparser
Test : <body><ruby><button><rp></rp></button></ruby></body>Spec : <body><ruby><button><rp></rp></button></ruby></body>
Opera, html5lib, IE: <body><ruby><button></button><rp></rp></ruby></body>
Safari, Firefox, htmlparser
Test : <body><table><li><li></li></table></body>Spec : <body><li></li><li></li><table></table></body>
Safari, Firefox, Opera, htmlparser, IE<body><li></li><table><li></li></table></body>
html5lib
4Some of the incompatibilities are caused by differences between versions of the
HTML5 specification, which is discussed below.
5Consumer Preview, version 10.0.8250.0.

We have investigated the second case for Firefox. The specification for thestart rp tag can be written as follows.
if isInScope[{Ruby}] then {generateImpliedEndTag[];
if !match[ {Ruby} .* ] then ERROR};
insertElement[me]The code of Firefox does not correspond to this, but to the specification
below. We found that this is compatible with the latest published version of thespecification, W3C Working Draft 25 May 2011, although we were working with
the Editor’s Draft 22 February 2012.
if isInScope[{Ruby}] then {generateImpliedEndTag[];
if !match[ {Ruby} .* ] then ERROR
while !match[ {Ruby} .*] do POP;};
insertElement[me]6<== Extra code in Firefox

Related WorkThe reachability analysis of pushdown systems with checkpoints was studied by
Esparza et al. as an application of LTL model checking of pushdown systems
with regular valuations [EKS03]. They presented a translation to ordinary pushdown systems. Although reachability can be decided via the translation, it is notpractical to apply the translation because of exponential blowup of the size of
pushdown systems. They also showed that the reachability problem of pushdown
systems with checkpoints is EXPTIME-complete.
Reachability can also be decided by translation to extensions of pushdown
systems such as alternating pushdown systems and stack automata [GGH67].
An analysis for alternating pushdown systems is given in [BEM97] and thatfor stack automata is given in [HO08] as reachability analysis for higher-order
pushdown systems. Although the translations to those systems do not incur
exponential blowup, their algorithms are more complicated than our reachability
analysis for conditional pushdown systems. An efficient algorithm for alternating
pushdown systems was developed in [SSE06,Suw09]. However, only an algorithm
for a restricted class with polynomial time complexity was implemented.

7Conclusions

We have developed a reachability analyzer for the HTML5 parser specification
based on the analysis of conditional pushdown systems. The analysis is applied tothe automated generation of HTML documents for path testing of the specification. Several compatibility issues in Web browsers and HTML5 parsing libraries
are found by supplying the documents to them.

One of the limitations of our work is that we cannot handle the specification
for formatting elements. This is because their specification requires destructive
manipulation of the stack. We are planning to address this limitation by checking
the reachability to the first point where a destructive operation on the stack isrequired.

References[BEM97] A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown
automata: application to model-checking. In CONCUR ’97, pages 135–150,
1997. LNCS 1243.
[Brz64] Janusz Brzozowski. Derivatives of regular expressions. J. ACM, 11:481–494,
1964.
[Con12] World Wide Web Consortium. HTML5: Editor’s draft 22 February 2012,2012. http://dev.w3.org/html5/spec/Overview.html.
[EHRS00] J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms
for model checking pushdown systems. In CAV 2000, pages 232–247, 2000.
LNCS 1855.
[EKS03] J. Esparza, A. Kucera, and S. Schwoon. Model checking LTL with regular valuations for pushdown systems. Information and Computation,
186(2):355–376, 2003.
[GGH67] S. Ginsburg, S. A. Greibach, and M. A. Harrison. Stack automata andcompiling. J. ACM, 14(1):172–201, 1967.
[HO08] M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis forhigher-order pushdown systems. Logical Methods in Computer Science, 4:1–
45, 2008.
[htm]
html5lib. html5lib. http://code.google.com/p/html5lib/.
[KN11] Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning, published online March
2011.
[LO10]
Xin Li and Mizuhito Ogawa. Conditional weighted pushdown systems andapplications. In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pages 141–150, 2010.
[Min05] Yasuhiko Minamide. Static approximation of dynamically generated Web
pages. In Proceedings of the 14th International World Wide Web Conference,
pages 432–441. ACM Press, 2005.
[ORT09] Scott Owens, John Reppy, and Aaron Turon. Regular-expression derivatives
re-examined. J. of Functional Programming, 19:173–190, 2009.
[SSE06] D. Suwimonteerabuth, S. Schwoon, and J. Esparza. Efficient algorithms foralternating pushdown systems with an application to the computation ofcertificate chains. In ATVA 2006, pages 141–153, 2006. LNCS 4218.
[Suw09] Dejvuth Suwimonteerabuth. Reachability in Pushdown Systems: Algorithms
and Applications. PhD thesis, Technischen Universität München, 2009.
[Val]
Validator.nu.
Thevalidator.nu
html
parser.
http://about.validator.nu/htmlparser/.