Model Checking Recursive Programs with
Numeric Data Types
Matthew Hague and Anthony Widjaja Lin
Oxford University Computing Laboratory

Abstract. Pushdown systems (PDS) naturally model sequential recursive programs. Numeric data types also often arise in real-world programs. We study the extension of PDS with unbounded counters, which
naturally model numeric data types. Although this extension is Turingpowerful, reachability is known to be decidable when the number of reversals between incrementing and decrementing modes is bounded. In thispaper, we (1) pinpoint the decidability/complexity of reachability andlinear/branching time model checking over PDS with reversal-bounded
counters (PCo), and (2) experimentally demonstrate the effectiveness of
our approach in analysing software. We show reachability over PCo is
NP-complete, while LTL is coNEXP-complete (coNP-complete for fixed
formulas). In contrast, we prove that EF-logic over PCo is undecidable.
Our NP upper bounds are by a direct poly-time reduction to satisfaction
over existential Presburger formulas, allowing us to tap into highly optimized solvers like Z3. Although reversal-bounded analysis is incomplete
for PDS with unbounded counters in general, our experiments suggestthat some intricate bugs (e.g. from Linux device drivers) can be discovered with a small number of reversals. We also pinpoint the decidability/complexity of various extensions of PCo, e.g., with discrete clocks.

1

Introduction

Pushdown systems (PDS) are natural abstractions of sequential programs withunbounded recursions whose verification problems have been extensively studied(cf. [4, 12, 35]). In addition to recursions, numerical data types commonly arise inreal-world programs. A standard approach to these potentially infinite domains
is to map them into abstract domains that are more amenable to analysis (e.g.
finite ones like {Pos, Neg, Zero}, or infinite ones expressed by intervals, difference
bound matrices, polyhedra, etc.). For other types of program analysis, it is also
common to simply ignore numerical data types. For a comprehensive treatmentof these techniques, and others, the reader is referred to the survey [11].
In this paper, we study a different approach. Motivated by the success of
pushdown systems (or similar models like boolean programs) in software model
checking (cf. [2, 3, 29]), we aim to investigate extensions of pushdown systems
with numerical data types and preserve nice properties, such as decidability andgood complexity. A clean and simple approach is to enrich pushdown systems
with unbounded counters, which can be incremented/decremented and tested
for zero. Unfortunately, this model is Turing-powerful, even without the stack.

2

Matthew Hague and Anthony Widjaja Lin

One way to retain decidability of reachability is to impose an upper boundr on the number of reversals between incrementing and decrementing modes
for each counter (cf. [9, 19]). In fact, decidability holds even if discrete clocks
are added to the model [9]. On the other hand, the complexity of reachability over these models is still open; a simple analysis of [9, 19] yields at least
double exponential-time complexity for their algorithms. Recently, the authorsof [13] observed that replacing the use of Parikh’s Theorem [24] in [19] by arecently improved version of [34] immediately yields an NP procedure for thisreachability problem (without clocks) for fixed numbers of reversals and counters, yielding only an NEXP procedure in general. Furthermore, the decidabilityof linear/branching time model checking over these models is also unknown.
There are at least two potential applications of reversal-bounded model
checking (cf. [9, 20]). First, it could be used as a sound but incomplete verification technique for the case of unbounded reversals. Despite this incompleteness,
results in bounded model checking suggest that “shallow” bugs are common
in practice (cf. [11]). Clearly, reversal-bounded model checking is an infinitestate generalization of bounded model checking over counter systems. A second
application is the use of reversal-bounded counters for tracking the number oftimes certain actions have been executed to reach the current configuration. For
example, we can check the existence of a computation path in a recursive program where the number of invocations for the functions f1 , f2 , f3 , and f4 are
the same. Similar counting properties (and their model checking problems) havebeen studied in many other contexts (cf. [22] and references therein).
Contributions. We begin by studying pushdown systems enriched withreversal-bounded counters, which can be compared against and incremented byconstants given in binary, but without clocks (PCo). This model is more generalthan the model studied in [13, 19], which allows only counters to be comparedagainst 0 and incremented by {−1, 0, 1}, though at the cost of an exponential
blow-up (cf. [20]) our model can be translated into their model. Our main contributions are (1) to pinpoint the decidability/complexity of reachability andlinear/branching time model checking over PCo, and (2) experimentally demonstrate the effectiveness of our approach in the analysis of software.
We show that reachability over PCo is NP-complete, while LTL model checking is coNEXP-complete (coNP-complete for fixed formulas). In contrast, we
prove that model checking EF-logic over PCo is undecidable. All of our lower
bounds hold already for PDS with one 1-reversal counter wherein numeric constants, which can be either be compared against or used to increment/decrement
counters, are restricted to 0 or 1. Our NP upper bounds are established by a direct
poly-time reduction to satisfaction over existential Presburger formulas, allowing
us to tap into highly optimized solvers like Z3 [10]. This reduction also permits
additional constraints on the number of actions executed and the values of thecounters at the end of the run (also specified in existential Presburger arithmetic)
without further computation overhead in the reduction. We have implemented
our algorithm and use it to analyse several examples, including some derived
from memory management issues in Linux device drivers. Although reversal-

Model checking recursive programs with numeric data types

3

bounded analysis is only complete up to the bound on the number of reversals,
our experiments suggest that many subtle bugs manifest themselves even withina small number of reversals, which our tool can detect reasonably fast. Without increasing complexity, our algorithm can also check whether a given PDS P
with unbounded counters is r-reversal bounded, for a given input r ∈ N; notethat this is not the same as deciding whether P is reversal-bounded, which isundecidable [14]. In the case when P is r-reversal bounded, our technique gives
a complete coverage of the infinite state space, which suggests the usefulness of
our technique in proving correctness as well as finding bugs.
We then study the extension of PCo with discrete clocks (PCC). We showthat LTL model checking over PCC is still coNEXP-complete, but hardness holds
even for a fixed formula. Similarly, we show that reachability over PCC is NEXPcomplete. We also show that, without reversal-bounded counters, model checking
EF-logic over PCC is EXPSPACE-complete even for a fixed formula.
Related work. The complexities of most standard model checking problems
over pushdown systems are well-understood. In relation to our results, we mention that LTL model checking over PDS is EXP-complete and is P-complete for
fixed formulas [4] (the latter is also the complexity for reachability), whereas
model checking EF-logic is PSPACE-complete [4, 35]. Therefore, adding reversalbounded counters yields computationally harder problems in both cases.
Over reversal-bounded counter systems (without stack), reachability is NPcomplete but becomes NEXP-complete when the number of reversals is given inbinary [18]. On the other hand, when the numbers of reversals and counters are
fixed, the problem is solvable in P [16]. The techniques developed by [16, 18],
which reason about the maximal counter values, are very different to our techniques, which exploit the connection to Parikh images of pushdown automata(first explicated in Ibarra’s original paper [19] though not in a way that gives optimal complexity or practical algorithm). For LTL model checking, the problem
is solvable in EXP even in the presence of discrete clocks [31], whereas EF-logic
model checking is still decidable but becomes undecidable for CTL [31].
For discrete-timed systems, reachability is known to be PSPACE-complete[1], where hardness holds already for three clocks [8]. Using region graph constructions [1], LTL model checking and EF-logic can also be easily shown to
be PSPACE-complete. Note that we do not consider timed logics (cf. [5]). The
complexities of pushdown systems with clocks have also been studied, e.g., [7].
Organization. §2 contains preliminaries. In §3, we define the basic model PCC
that we study. §4 and §5, contain upper and lower bounds for model checking
PCo. In §6, we extend our results to PCC. Experimental results are given in §7.
Other extensions and future work are given in §8. Due to the space limit, some
proofs are in the full version from the project page http://www.cs.ox.ac.uk/recount.

2

Preliminaries

Transition systems. An action alphabet ACT is a finite nonempty set of actions. A transition system over ACT is a tuple S = hS, {→a }a∈ACT i, where S

4Matthew Hague and Anthony Widjaja Lin

is a set of configurations and each →a ⊆ S × S is an a-labeled transition relation containing the set of all a-labeled transitions. We use → to denote theunion of all →a . A (computation) path in S is a finite or infinite sequence
π = α0 →a1 α1 →a2 . . . such that αi ∈ S, αi →ai+1 αi+1 and ai ∈ ACT foreach i. If π is finite, let last(π) denote the last configuration in π. In this case,a1 a2 . . . is said to be a (finite) trace in S from α0 to last(π). Automata We
assume familiarity with automata theory. In particular, nondeterministic Büchi
automata (NBWA), cf. [32], and pushdown automata (PDA), cf. [27]. For an
NBWA A, we denote by L(A) the language recognized by A. Similarly, given a
PDA we also write L(P) for the language P recognizes.
Parikh images Given an alphabet Σ = {a1 , . . . , ak } and a word w ∈ Σ ∗ , wewrite P(w) to denote a tuple with |Σ| entries where the ith entry counts thenumber of occurrences of ai in w. Given a language L ⊆ Σ ∗ , we write P(L) to
denote the set {P(w) : w ∈ L}. We say that P(L) is the Parikh image of L.
Logic The syntax of LTL (cf. [17, 31, 32]) over ACT is given by: ϕ, ϕ′ := a (a ∈ACT) | ¬ϕ | ϕ∨ϕ′ | ϕ∧ϕ′ | Xϕ | ϕUϕ′ . Given an ω-word w ∈ ACTω and an LTL
formula ϕ over ACT, we define the satisfaction relation w |= ϕ in the standard
way. Write [[ϕ]] for all w ∈ ACTω such that w |= ϕ. EF-logic (over ACT) is a
fragment of CTL (cf. [17, 31]) with the syntax ϕ, ψ := ⊤ | ¬ϕ | ϕ ∨ ψ | haiϕ (a ∈ACT) | EFϕ. Given an EF formula ϕ, a transition system S = hS, {→a }a∈ACT iand s ∈ S, we may define S, s |= ϕ in the standard way.
Presburger formulas Presburger formulas are first-order formulas over natural
numbers with addition. Here, we use extended existential Presburger
formulasP∃x1 , . . . , xk .ϕ where ϕ is a boolean combination of expressions ki=1 ai xi ∼ b forconstants a1 , . . . , ak , b ∈ Z and ∼∈ {≤, ≥, <, >, =} with constants represented
in binary. It is known that satisfiability of existential Presburger formulas is
NP-complete even with these extensions (cf. [26]).

3

Pushdown systems with counters and clocks

The model. An atomic clock constraint on clock variables Y = {y1 , . . . , ym } issimply an expression of the form yi ∼ c or yi − yj ∼ c, where ∼ ∈ {<, >, =},1 ≤ i, j ≤ m and c ∈ Z. An atomic counter constraint on counter variables
X = {x1 , . . . , xn } is simply an expression of the form xi ∼ c, where c ∈ Z.
A clock-counter (CC) constraint θ on (X, Y ) is simply a boolean combinationof atomic counter constraints on X and atomic clock constraints on Y . Givena valuation ν : X ∪ Y → N to the counter/clock variables, we can determine
whether θ[ν] is true or false by replacing a variable z by ν(z) and evaluting theresulting arithmetic expressions in the obvious way. Let ConstX,Y denote the setof all CC constraints on (X, Y ). Intuitively, these formulas will act as “enabling
conditions” (or “guards”) to determine whether certain transitions can be fired.
A pushdown system with n counters and m discrete clocks is a tuple P =(Q, ACT, Γ, δ, X, Y ) where (1) Q is a finite set of states, (2) ACT is a set ofaction labels, (3) Γ is a stack alphabet, (4) X = {x1 , . . . , xn } is a set of counter
variables, (5) Y = {y1 , . . . , ym } is a set of clock variables, and (6) δ is a transition

Model checking recursive programs with numeric data types

5

relation of P, which is defined to be a finite subset of (Q×Γ ∗ ×ConstX,Y )×ACT×(Q×Γ ∗ ×2Y ×Zn ). A configuration of P is a tuple (q, u, u, v) ∈ Q×Γ ∗ ×Nn ×Nm .
Given a ∈ ACT and two configurations α1 = (q, u, u, v) and α2 = (q ′ , u′ , u′ , v′ )of P, α1 →a,P α2 iff there exists h(q, w, θ), a, (q ′ , w′ , Y ′ , w)i ∈ δ such that– θ holds under the valuation (u, v),– for some v ∈ Γ ∗ , u = wv and u′ = w′ v,– if Y ′ = ∅, then each clock progresses by one time unit, i.e., v′ = v + 1; if
Y ′ 6= ∅, then the clocks in Y ′ are reset, while other clocks do not change,i.e., for each yi ∈ Y , set vi′ := 0 and, for each yi ∈/ Y , set vi′ := vi .
′′– u := u + w (note, all elements of u must be non-negative).
The transition system generated by P is SP = hS, {→a }a∈ACT i, where S denotes
the set of configurations of P and →a is defined to be →a,P .
Notice that in this model, which is similar to the model given in [9], clocks
are updated via transitions. This is slightly different from the usual definitionof discrete timed systems (cf. [1]) in which (1) clocks may progress within any
particular state of the system without taking any transitions as long as someinvariants are satisfied, and (2) transitions are instantaneous. However, by introducing self-looping transitions with no reset and adding an extra “dummy”
clock which always resets for old transitions, we can easily construct a weakly
bisimilar system in our model. See [9] for more details.
Let us now define the r-reversal-bounded variant of this model for each r ∈N. Syntactically, a pushdown system with n r-reversal bounded counters and mdiscrete clocks is simply a pair (r, P) of number r and a pushdown system P withn counters and m clocks. Together with a given initial configuration α of P, thesystem (r, P) generates a transition system Sα(r,P) = hS, {→a }a∈ACT i defined
as follows. Let SP = hS ′ , {→′a }a∈ACT i be the transition system generated by
P. A path π in SP from α is said to be r-reversal-bounded if each counter of
P changes from a non-incrementing mode to non-decrementing mode (or viceversa) at most r times in the path π. For example, if the values of a counter x ina path π from α are 1, 1, 1, 2, 3, 4, 4, 4, 3, 2, 2, 3, then the number of reversals of x
is 2 (reversals occur in between the overlined positions). This sequence has threephases (i.e. subpaths interleaved by consecutive reversals or end points): nondecrementing, non-incrementing, and finally non-decrementing. This intuition
suffices for understanding the main ideas in this paper, though we provide thedetailed definitions in the full version. The set S is then defined to be the set of
all finite r-reversal-bounded paths from α. Given two such paths π and π ′ suchthat π ′ = π, α′ , we define π →a π ′ iff last(π) →′a α′ . Notice that Sα(r,P) is a tree.
We write (r, n, m)-PCC to denote the set of all pushdown systems with n
r-reversal-bounded counters and m discrete clocks. We write PCC to denote theunion of all (r, n, m)-PCC for all r, n, m ∈ N. Similarly, we use (r, n)-PCo todenote (r, n, 0)-PCC and (r, m)-PCl to denote (r, 0, m)-PCC. We use PCo andPCl as well in the same way.
Unless stated otherwise, we make the following conventions: (1) the number
r of reversals is given in unary, and (2) numeric constants in CC constraints

6

Matthew Hague and Anthony Widjaja Lin

and counter increments are given in binary. In the sequel, we will deal with(control-state) reachability, model checking LTL and EF over PCC (and theirvariants) defined as follows:– Reachability: given a PCC P and two configurations α, α′ of P (in binary
representation), decide whether α′ is reachable in Sα
P.
– Control-state reachability: given a PCC P and two states q, q ′ of P, decide
whether there exist stack contents u, u′ ∈ Γ and counter values c, c′ ∈ Nk
(q,u,c).
such that (q ′ , u′ , c′ ) is reachable in SP– LTL model checking: given a PCC P, a configuration α of P (in binary),
and an LTL formula ϕ, decide whether Sα
P , α |= ϕ.
– EF model checking: given a PCC P, a configuration α of P (in binary), andan EF formula ϕ, decide whether Sα
P , α |= ϕ.

4Upper bounds for model checking PCo

In this section, we show that reachability over PCo is in NP by providing a
direct poly-time reduction to satisfactions of existential Presburger formulas.
As applications of our technique, we will provide: (1) an NP upper bound forcontrol-state reachability with additional constraints on counter values at the
beginning/end of the run and how many times actions are executed at the endof the run, and (2) a coNEXP upper bound for LTL model checking over PCo(coNP for fixed formulas). Lower bounds are proved in the next section.
An NP procedure for reachability over PCo. We prove the following.
Theorem 1. Reachability over PCo is NP-complete. In fact, it is poly-time reducible to checking satisfactions of existential Presburger formulas.
Given an (r, k)-PCo P = (Q, ACT, Γ, δ, X), and two configurations α = (q, u, c)and α′ = (q ′ , u′ , c′ ) of P, our algorithm decides if α′ is reachable from α in SP .
Let c = (c1 , . . . , ck ) and c′ = (c′1 , . . . , c′k ). We assume that u = u′ = ⊥ since,by hardwiring u and u′ into the finite control of P the standard way, the PCo
P may initialize the stack content to u and make sure the final stack content
is precisely u′ . In addition, let d1 < . . . < dm denote all the numeric constants
appearing in an atomic counter constraint as a part of CC constraints in P.
Without loss of generality, we assume that d1 = 0 for notational convenience.
Let REG = {ϕ1 , . . . , ϕm , ψ1 , . . . , ψm } be a set of formulas defined as follows. Notethat these formulas partition N into 2m pairwise disjoint regions.
ϕi (x) ≡ x = di ,ψi (x) ≡ di < x < di+1 (1 ≤ i < m),ψm (x) ≡ dm < x .

A vector v in Modes = REGk × [0, r]k × {↑, ↓}k is said to be a mode vector.
Given a path π = α0 α1 . . . αh from α to α′ , we may associate a mode vector vj
to each configuration αi in π that records for each counter: which region its value
is in, how many reversals its used, and whether its phase is non-decrementing (↑)
or non-incrementing (↓). Consider the sequence σ = {vj }hj=0 of mode vectors. A

Model checking recursive programs with numeric data types

7

crucial observation is that each mode vector v ∈ Modes in this sequence occurs
in a contiguous block, i.e., if 0 ≤ j ≤ j ′ ≤ h are such that vj (resp. vj ′ ) is the first(resp. last) time v appearing in σ, then vl = v for all l ∈ [j, j ′ ]. Intuitively, oncea change occurs in σ, we cannot revert to the previous vector. This is because
any such change will incur an extra reversal for at least one counter. There areat most Nmax := |REG| × (r + 1) × k = 2mk(r + 1) distinct mode vectors in σ.
In outline, to avoid an exponential blow-up in our reduction, we will first
construct a very rough “upperapproximation” of the PCo P as a PDA P ′ . Intuitively, P ′ will simulate P, while guessing and remembering only how manymode vector changes have occurred, but disregarding the counter information.
In this case, there are runs in P ′ that are not valid in P. Each time P ′ fires atransition t (derived from a transition t′ of P by disregarding counters), it will
also output information about the counter tests and in(de)crements associatedwith t′ , and how many changes in the mode counter have occurred thus far(recorded in the states of P ′ ). Since P ′ is of polynomial size, we apply on P ′ thelinear-time algorithm of Verma et al. [34] to compute the Parikh images of CFGs
(equivalently, PDA). Building on the output formula, we use further existential
quantifications to guess the evolution of the mode vectors, on which we impose
further constraints to eliminate invalid runs. We give the details below.
Building the PDA P. Define P ′ = (Q′ , ACT′ , Γ, δ ′ , (q, 0), F ′ ) allowing transitions
to execute a (finite) sequence of actions, instead of just one. These are for convenience and can be encoded in the states of P ′ . Let Q′ = Q × [0, Nmax − 1] anddefine ACT′ implicitly from δ ′ . In fact, ACT′ is a (finite) subset of {(ctri , u, j, l) :i ∈ [1, k], u ∈ Z, j ∈ [0, Nmax − 1], l ∈ {0, 1}} ∪ (ConstX,∅ × [0, Nmax − 1]). Here,l ∈ {0, 1} signifies whether this action changes the mode vector. We define δ ′ byinitially setting δ ′ = ∅ and adding rules as follows. If h(q, w, θ), a, (q ′ , w′ , u)i ∈ δwhere u = (u1 , . . . , uk ) then for each i ∈ [0, Nmax − 1] we addh((q, i), w), (θ, i)(ctr1 , u1 , i, 0)(ctr2 , u2 , i, 0) . . . (ctrk , uk , i, 0), ((q, i), w′ )ito δ ′ . If i ∈ [0, Nmax − 1), we also add the following rule:h((q, i), w), (θ, i)(ctr1 , u1 , i, 1)(ctr2 , u2 , i, 1) . . . (ctrk , uk , i, 1), ((q, i + 1), w′ )iIn this way, P ′ makes “visible” the counter tests and the counter updates performed. Finally, the set F ′ of final states are defined to be {q ′ } × [0, Nmax − 1]and the initial control state is (q, 0).
Constructing the formula. Fix an ordering on ACT′ , say α1 < . . . < αl . For
convenience, by f we denote a function mapping αi to i for each i ∈ [1, l].
We apply the linear-time algorithm of [34] on P ′ above to obtain χ(z), wherez = (z1 , . . . , zl ), such that for each n ∈ Nl we have n ∈ P(L(P ′ )) iff χ(n) holds.
We impose constraint χ to eliminate vectors that do not correspond to traces of
P ′ . Currently, P ′ knows only the maximum number of allowed changes in mode
vectors, but is not “aware” of other information about the counters. Therefore,
the formula that we construct should assert the existence of a valid sequence ofmode vectors that respect the counter tests and updates that P ′ outputs. We

8Matthew Hague and Anthony Widjaja Lin

construct HasRun of the form
Init(m0 ) ∧ GoodSeq(m0 , . . . , mNmax −1 ) ∧ χ(z)∧∃z∃m0 , . . . , mNmax −1
Respect(z, m0 , . . . , mNmax −1 ) ∧ EndVal(z)where m0 , . . . , mNmax −1 are variables for representing a valid sequence of mode
vectors occurring in the run of P.
Let us now elaborate HasRun. First, since a mode vector is a memberof Modes = REGk × [0, r]k × {↓, ↑}k , we set mi to be a tuple of variables{regij , revij , arrij : j ∈ [1, k]}, where:– regij is a variable that will range over [1, 2m] denoting which region the jthcounter is in (a number of the form 2i + 1 refers to ϕi , while 2i refers to ψi ).
– revij is a variable that will range over [0, r] denoting the number of reversals
that have been used thus far by the jth counter.
– arrij is a variable that will range over {0, 1} denoting the current arrow
direction, e.g., 0/1 for ↑/↓ (non-decrementing/non-incrementing mode).
Using Init(m0 ), we assert that the initial mode vector needs to respect thegiven initial configuration α = (q, u, c), where c = (c1 , . . . , ck ). More precisely,
V !
m 
k
^
^
reg0j = 2i − 1 ↔ ϕi (cj )0.
revj = 0 ∧Init(m0 ) ≡reg0j = 2i ↔ ψi (cj )
i=1

j=1

In fact, since c is given, we could replace some of these variables by constants.
However, being able to define this in the formula allows us to prove something
more general, as we will see later.
Recall that the target configuration is α′ = (q ′ , u′ , c′ ), where c′ = (c′1 , . . . , c′k ).
We assert that the end counter values match c′ . This definition is given as follows.
Note, multiplications by constants are allowed within Presburger arithmetic.


k
r
^
X
X

d × zf (ctrj ,d,i,l)  = c′j .
EndVal(z) ≡j=1

i=0 (ctrj ,d,i,l)∈ACT′

We define GoodSeq(m0 , . . . , mNmax −1 ) to express that m0 , . . . , mNmax −1 isa valid sequence of mode counters. The formula is a conjunction of smaller
formulas defined below. One conjunct says that each revij must be a number in[0, r]. Likewise, we add conjuncts expressing that each regij (resp. arrij ) ranges
over [1, 2m] (resp. {0, 1}). We also need to state that changes in the direction
arrows incur an extra reversal (otherwise, no reversal is incurred):k Nmaxk Nmax^−2  arri 6= arri+1 → revi+1 = revi + 1 V 
^
^−1
^
j
j
j
j
.
0 ≤ revij ≤ r. ∧arrij = arri+1→ revi+1= revij
j
j
j=1

j=1

i=0

i=0

max −1max −1:
must obey the changes in {arrij }NFinally, the sequence {regij }N
i=0
i=0

k Nmax
^
^−2 

j=1

i=0

=0
regij < regi+1→ arri+1
j
j

^


=1 .
regij > regi+1→ arri+1jjModel checking recursive programs with numeric data types

9

I.e., since regions denote increasing intervals, going to higher (resp. lower) regions
mean the counter mode must be non-decrementing (resp. non-incrementing).
Lastly, we give Respect(z, m0 , . . . , mNmax −1 ). Again, this is a conjunction.
First, when the jth counter is non-incrementing (resp. non-decrementing), weallow only non-negative (resp. non-positive) counter increments:
k Nmax^^−1  arrij = 0 →

j=1

V
V
(ctrk ,d,i,l)∈ACT′ ,d<0 zf (ctrk ,d,i,l) = 0
V.
arrij = 1 → (ctrk ,d,i)∈ACT′ ,d>0 zf (ctrk ,d,i,l) = 0

i=1

Secondly, the value of the jth counter at the beginning and end of each modemust respect the guessed mode vector. Let us first introduce some notations.
Observe that the value
jth counter at the end of ith mode vector can beP of theP
i−1 P
expressed by cj +(ctrj ,d,i,0) d ×
i′ =0(ctrj ,d,i′ ,l)∈ACT′ d × zf (ctrj ,d,i′ ,l) +zf (ctrj ,d,i,0) . Let us denote this term by EndCounterij . Similarly, the value at thePi−1 P
beginning of the ith mode is cj + i′ =0 (ctrj ,d,i′ ,l)∈ACT′ d × zf (ctrj ,d,i′ ,l) . We
denote this term by StartCounterij . Hence, this second conjunct isV
k Nmaxm ^^−1 ^regi = 2l − 1 → (ϕl (EndCounteri ) ∧ ϕl (StartCounteri ))
j

j=1

i=0

j

j

regij = 2l → (ψl (EndCounterij ) ∧ ψl (StartCounterij ))l=1.

Finally, we need to express that no invalid counter tests are executed in a given
mode. To test whether a CC constraint θ is satisfied by the values b = (b1 , . . . , bk )of the counters, it is necessary and sufficient to test whether θ is satisfied bysome vector b′ = (b′1 , . . . , b′k ), where each bi lies in the same region in REG as
b′i . Therefore, the desired property can be expressed as:
Nmax
^−1
i=0

^

zf (θ,i) > 0 → θ(StartCounteri1 , . . . , StartCounterik ).

(θ,i)∈ACT′

Of course, we might want to make the formula smaller by associating new variables for all terms StartCounterij and EndCounterij . Since the translation from
PDA to CFGs produces an output of cubic size, it is easy to check that the sizeof HasRun is cubic in kPk, r, and k.
Applications. We start with a straightforward application of the above proof:
Control-state reachability over PCo with additional existential Presburger constraints on counter values at the beginning/end of the run and on how manytimes actions are executed at the end of the run can be checked in NP. In fact,
it is poly-time reducible to checking satisfactions over existential Presburger formulas. To see this, observe that the counter values in α and α′ , which weretreated as constants in HasRun, could be treated as variables. Hence, we can add
the additional constraint within the inner bracket of HasRun as a conjunct, andquantify the new variables for counter values. Secondly, we have the following:
Theorem 2. LTL model checking over PCo is coNEXP-complete. For fixed formulas, it is coNP-complete.

10

Matthew Hague and Anthony Widjaja Lin

For this, we begin with the standard Vardi-Wolper automata-theoretic approach[32] reducing the complement of this problem to recurrent reachability over PCo:
given a PCo P = (Q, ACT, Γ, δ, X) and a subset F ⊆ Q, decide if there is a run of
P visiting configurations of the form (q, u, c) where q ∈ F infinitely often. This
reduction obtains an NBWA of exponential size from the negation of the given
LTL formula, and builds the product of this NBWA and P. Thus, the reduction
is exponential in the LTL formula but polynomial in the PCo. Therefore, itsuffices to show that recurrent reachability is in NP. Observe that all infinite
runs π of P stabilise in some mode, expressed by a mode vector m. We split πinto a subpath from the initial configuration α to a configuration α′ = (q ′ , u′ , c′ )in π in mode m, and the rest of the path from α′ . In fact, if c′ = (c′1 , . . . , c′k ),then α′ could be chosen such that if the value of the jth counter after α′ in π has
a maximum c (e.g. when jth counter value stabilises in a region < 2m, which isbounded), then c′j = c. By allowing only rules which do not decrement counters
whose values do not stabilise, we may treat the path from α′ as a path of a PDS
with no counters. Hence, we use a well-known lemma of PDS (w.l.o.g. assume
that transitions of PDS/PCo only check the top stack character):Lemma 3 ([4]). Given a PDS P = (Q, ACT, Γ, δ), an initial configuration α,
and a set F ⊆ Q, then there exists an infinite computation path of P from α visiting F infinitely often iff there exist configurations (p, α) ∈ Q × Γ , (g, u), (p, αv)
such that g ∈ F and (i) α can reach (p, αw) for some w ∈ Γ ∗ , and (ii) (p, α)
can reach (g, u), from which (p, γv) is reachable.
We construct a PCo P ′ that simulates P (for the initial subpath of the recurrent
reachability witness). Eventually, it decides to stop simulating P at some configuration (p, αw, v). The state and the top-stack character are then made visible
by P ′ with an action (p, α). The PCo P ′ then empties the stack and continues
the simulation of P from (p, α) except that (1) only rules which increment counters by non-negative values are allowed, but instead of actually modifying thecounter values, actions of the form +ctrj will be executed if the rule increments
the jth counter by a positive value (2) counter tests θ are no longer performed,
but instead we execute actions that signify θ. When a configuration of the form(g, u, v) is reached with g ∈ F , it will make it visible by performing an actionof the form g!. At any given time after this, it may output a character (p′ , α′ ),where p′ is the current state and α′ is the current top stack character, and go
into the state Finish. There exists a computation path of P from α that visits
F infinitely often iff there exists a path from α to the Finish in P ′ such that:(a) the number executions of some (p, α) is 2, (b) some g! action has been executed, (c) if the region of the end value of the jth counter (corresponding to
the jth counter value of the initial witnessing subpath of P) is bounded (i.e.
< 2m), then no action +ctrj must have been executed, and (d) no counter test
actions violating the regions of the end counter values have been executed. Using
the techniques from Theorem 1, we may express these constraints as a poly-size
existential Presburger formula. In conclusion, we have reduced recurrent reachability over PCo to control-state reachability over PCo with constraints, which
we already saw to be in NP.

Model checking recursive programs with numeric data types

511

Lower bounds for model checking PCo

In this section, we prove coNEXP and coNP lower bounds for model checking
LTL and reachability over PCo. We will also show that model checking EF-logic
is undecidable even for a fixed formula. All our lower bounds hold for (1, 1)-PCo
where counters can only be compared against 0 and incremented by {−1, 0, 1}.
Lower bound for LTL and reachability We start with coNP-hardness for a
fixed LTL formula over (1, 1)-PCo. We show that the complement of this model
checking problem is NP-hard. It will be clear later that the same proof can beused to show that reachability is NP-hard over (1, 1)-PCo. The idea is to reducefrom the NP-complete 0-1 Knapsack problem ([23]): given a1 , . . . , ak , b ∈ N in
Pkbinary, decide whether i=1 ai xi = b for some x1 , . . . , xk ∈ {0, 1}. The reduction constructs a (1, 1)-PCo P which initializes the counter to 0 and repeats
for each i ∈ [1, k]: guess xi , add ai xi to the counter. The PCo then checks
whether the counter is b by substracting b and checking whether the result
is 0. If the test is positive, execute a special action success and then loop
silently. The LTL formula is G¬success. Note, this PCo makes one reversal.
The problem with this reduction, however, is that the numbers a1 , . . . , ak , b
are given in binary, whereas each transition in P can add −1 or 1. Hence,
we cannot naively hardwire the “intermediate” values of a1 , . . . , ak , b during
the computation in the finite control. Instead, we need to use the stack.
We illustrate this technique by the exx := x + 1
ample in the following figure on the
1→0
0→ǫ
0→ǫ
0→ǫ
right. This is a PCo with one counter 0
1
2
3
x that increases x by the number rep1→01→01→0x := x + 1
resented by the topmost four bits on
ǫ→1
0’
1’
2’
the stack (edge label u → v defines
ǫ→1
ǫ→1
the stack operation). For example, if
the PCo starts with the configuration (3, 1101, 0), then it will end at the configPk
uration (0, 0, 13). Using this technique, we will only need at most i=1 log(ai ) +log(b) extra states and therefore avoiding an exponential blow-up.
For the coNEXP lower bound for non-fixed formulas, we reduce succinct 0-1
Knapsack. We define Succinct 0-1 Knapsack as the 0-1 Knapsack problem
where the input is given as a boolean formula θ with variables x1 , . . . , xk+m wherek, m ∈ Z>0 are given in unary. Here θ represent the numbers a1 , . . . , a2k −1 , b ∈ Neach with precisely 2m bits (leading 0s permitted) as follows:– The ith bit of bin(b) is defined to be x ∈ {0, 1} iff the formula θ evaluatesto x when x1 , . . . , xk+m are evaluated to 0k binm (i).
– The ith bit of bin(aj ) is defined to be x ∈ {0, 1} iff the formula θ evaluatesto x when the inputs to x1 , . . . , xk+m are bink (j)binm (i).
P k
The problem is to check whether 2i=1−1 ai zi = b for some z1 , . . . , z2k −1 ∈ {0, 1}.
The problem of Succinct 0-1 Knapsack can be shown to be NEXP-complete in
the same way that the problem Succinct Knapsack, where natural numbers canbe assigned to zi ’s (instead of only {0, 1}), is shown in [33] to be NEXP-complete.

12

Matthew Hague and Anthony Widjaja Lin

We now show a NEXP lower bound for the complement of LTL model checking over (1, 1)-PCo by reducing from Succinct 0-1 Knapsack. The idea of the
reduction is the same as for the case of fixed formulas, but we will have to use
the LTL formula to count up to doubly exponential values.
The stack alphabet includes #, c01 , c11 , . . . , c0m , c1m . If the ith bit of aj is 1 andzj has been guessed to be 1, then we need to add 2i to the counter. E.g., suppose
we’re on the 11 . . . 1th bit of the a0 . Using the techniques below, we calculatemthe value of this bit. If it is 1, we increment 2(2 −1) times. To do this, we push
the following sequence on the stack, again using techniques described below.
0c0m . . . c01 #0c1m c0m−1 . . . c01 # . . . . . . . . . #0c1m . . . c11 #(*)

That is, a bit-string with 2m many 0s, annotated with their bit positions (leastsignificant bit on the top/left of the stack). From this stack configuration, thesystem counts up to 1c0m . . . c01 #1c1m c0m−1 . . . c01 # . . . . . . . . . #1c1m . . . c11 #, i.e., ambit-string with 2m many 1s, taking 2(2 −1) steps. We increment the counter +1
at each step.
To complete the proof, we need to know how to: (1) enumerate all assignments
to x1 , . . . , xk+m and evaluate θ, (2) initialise the large counter described above,and (3) increment the large counter from 00 . . . 0 to 11 . . . 1.
Problem 1: We store the current assignment on the bottom of the stack, using x01 , x11 , . . . , x0k+m , x1k+m . Initially, we push x01 , . . . , x0k+m , making the pushedcharacters visible using suitable action symbols. We then guess whether θ evaluates to 1. An LTL formula encoding θ asserts this guess is correct. To move tothe lexicographically next assignment, we erase the stack, making the characters
visible, and then guess the next assignment, using the LTL to check it.
Problem 2: Guess and push 0cy11 . . . cymm #, using the formula to check thism1
on the stack. We then push 0cY1 1 . . . cYmm # (with, . . . , xyk+mmatches the xyk+1
the values of Y1 , . . . , Ym ∈ {0, 1} guessed) to the stack. This is done arbitrarily
many times and the PCo may stop at some point. To make sure we obtain (*)
on the top of the stack, we assert the successor property using the LTL formula.
Problem 3: This uses the idea for the fixed formula case: pop from the stack until
the first 0, then push a correct number of 1s annotated with the bit positions.
For this, an LTL formula asserts the successor property, cf. [28].
Undecidability results for EF-logic We now turn our attention to model
checking EF-logic over PCo. It turns out that the problem is already undecidable
for a fixed formula with two operators. We reduce from the emptiness of linear
bounded Turing machines (LTM), which is undecidable (cf. [27]). Given an LTM
M that accept/rejects an input w using at most c|w| space, we compute a (1, 1)PCo P, an EF formula ϕ, and a start state q0 of P such that SP , (q0 , ǫ) |= ϕiff M is nonempty. We make P guess a word w and an accepting computation
path of M, which is stored in the stack. The length c|w| is stored in the counter.
Once the path has been guessed, it suffices to show that: (P1) the length ofeach guessed configuration is c|w|, and (P2) each non-initial configuration is a
successor of its previous configuration. The guessing and checking stages incur
one alternation for the EF formula. Since checking P2 requires us to check at

Model checking recursive programs with numeric data types

13

most four consecutive tape cells of M (once a cell is chosen), we can remember
this location by decrementing the counter, moving to the previous configurationof M that is stored in the stack, and then further decrementing the countermaking sure that the end value is 0. See the full version for the proof.
Theorem 4. Model checking EF-logic over (1, 1)-PCo is undecidable even for a
fixed formula with two EF operators.

6

Adding clocks

To extend our results to the case of PCC, we use the region construction of Alurand Dill [1] to reduce a PCC to a PCo of exponential size (in exponential time)such that every run of the PCC can be projected, state-for-state, onto a runof the PCo. From S4, we obtain a coNEXP (resp. NEXP) upper bound for LTL
model checking (resp. reachability) over PCC. We next provide a lower bound.
Theorem 5. Reachability is NEXP-hard for PDS with discrete clocks and one
1-reversal-bounded counter. When clock constraint constants are given in binary, only three clocks and one single-reversal counter are needed. Similarly,
LTL model-checking is coNEXP-hard, even for a fixed formula.
We first consider unary constants, and a non-fixed number of clocks. We
adapt the previous reduction from Succinct 0-1 Knapsack, except the formulacan no longer be used to evaluate the boolean formulas. Instead, we encode bitswith two clocks, which are equal iff the bit is 1. We evaluate boolean formulas
using the transition guards. To test all assignments to x1 , . . . , xk+m we store
the valuation in the counters (not the stack). This is straightforward. Then, tobuild the large counter on the stack, we use another set of clocks to store the bit
position values of the last two blocks pushed on to the stack. These clocks canbe used to ensure the successor relation between the two values. For binary clock
constraints, we use Courcoubetis and Yannakakis [8] to reduce to three clocks.
Recall that model checking EF-logic over PCo is undecidable. It turns outthat this problem is decidable over PCl. See the full version for a proof.
Theorem 6. Model checking EF over PCl is EXPSPACE-complete. The lower
bound holds for fixed formulas with two clocks with binary constraint constants,
or with a non-fixed number of clocks when the constraints are in unary.

7

Experimental Results

We provide a prototypical C++ implementation of an optimised version of the
reduction in Section 4. In particular, from the Verma et al., we can derive, at
no cost, the number of times each rule of the PCo is fired. From this, we infer the number of action symbols output, and hence, do not need additionalvariables and transitions for these. In addition, the per mode information per
counter uses a single variable. Finally, we look for pairs of pushdown rules

14

Matthew Hague and Anthony Widjaja Lin

h(q1 , a1 , ⊤), ǫ, (q2 , a2 , ∅, ∅n )i and h(q2 , a2 , ⊤), ǫ, (q3 , a3 , ∅, ∅n )i such that a1 and a2
are single characters and the pair q2 , a2 does not appear together in any otherrule. Furthermore, a2 does not appear in a rule h(q, w, θ), a, (q ′ , w′ a2 w′′ , Y, w)iwhere |w′ | > 0. These rules can be replaced by h(q1 , a1 , ⊤), ǫ, (q3 , a3 , ∅, ∅n )i. Then
we remove unreachable productions from the generated CFGs. We used the 64bit Linux binary of Z3 2.16 [10] on the Presburger formulas on a quad-core, 2.4Gz
Intel R Xeon R machine with 12GB of RAM, running FedoraTM 12. We report thetime from the Linux command time for the translation and the run of Z3.
Double free in dm-target.c. In version 2.5.71 of the Linux kernel, a double
free was introduced to drivers/md/dm-target.c [30]. This was introduced to fix
a perceived memory-leak. When registering a new target, memory was allocatedand a check made to see if the target was already known. If so, it was freed andan “exists” flag set. Otherwise the target was added to the target list. Before
returning, the exists flag was checked and the object was freed (again) if it wasset. We created, by hand, a model of this file using a counter to store the lengthof the target list. The complete control flow of the file was maintained and data
only tracked when relevant to the memory management. The model outputs
special symbols to mark when memory is allocated or freed. We then look for a
run where, either an item was removed from the empty list, the number of freecalls was greater than the number of allocations, or, the code exited normally,
but more memory was allocated than freed. We were able to verify that the code
contained a memory error in version 2.5.71 and that the memory management
was correct in earlier versions (for a bounded number of reversals) provided as
many targets were registered as unregistered. Note, the counter is required to
track the size of the list which ensures that the number of allocations matches thenumber of frees. The size of the dm-target.c is approximately 175 lines without
comments. Detecting the bug took 2s, and proving correctness took 1.7s, 2.9s,
16s, 24s and 77s for 1, 2, 3, 4 and 5 reversals respectively.
Memory leak in aer inject.c. In version 2.6.32 of the Linux kernel, thefile drivers/pci/pcie/aer/aer inject.c contains a memory leak that waspatched in the next version [25]: two lists of allocated objects are maintained,
but, when exiting, the code empties the items from the first list and frees them,then, empties and frees the first list again, instead of the second. We created amodel of this driver with two counters to track the size of the lists and searched
for memory errors as in the previous example. Only one reversal was required
to detect the memory leak. We showed that the patch corrects the problem (upto one reversal). Note, without counters, it would always be possible for thenumber of allocations to differ from the number of frees. The file aer inject.c
is approximately 470 lines without comments. Detecting the bug required 220s
and proving correctness for a single reversal took 508s.
Buffer overflow. Jhala and McMillan have a buffer overflow example which
their technique, SatAbs and Magic, failed to verify [21]. There are three buffers,
x, y and z of sizes 100, 100 and 200 and two counters i and j. First, i is used tocopy up to 100 positions of x into z. Then, counters i and j are used to copy up
to 100 positions of y into the remainder of z. There is overflow if i, which indexes

Model checking recursive programs with numeric data types

15z, finishes greater than 199. This simply encodes into our model1 and could beverified correct (since the example is trivially reversal bounded) in 1.6s.
David Gries’s coffee can problem [15]. We have an arbitrary number ofblack and white coffee beans in a can. We pick two beans at random. If they are
the same colour, they are discarded and an extra black bean is put in the tin.
If they differ, the white is kept but the black discarded. The last bean in the
can is black iff the number of white beans is odd. This problem can be modelled
without abstraction by using the stack to count the number of black beans, anda single-reversal counter to track the number of white beans. We verified in 1.3s
that the last bean cannot be white if the number of white beans is odd, and in
1.1s that the last bean may be white if the number of white beans is even.

8

Extensions and Future Work

We prove, in the full version of this paper, that (i) reachability and LTL fora prefix-recognisable version of PCo is NEXP-complete and coNEXP-complete
respectively, even with one 1-reversal-bounded counter and a fixed formula; (ii)
LTL model checking for a fixed formula is coNEXP when the number of reversals
is given in binary, whereas reachability is in NEXP (a matching lower bound is in[18], even without the stack); and (iii) the reachability problem for second-order
pushdown systems (cf. [17]) with reversal bounded counters is undecidable.
For future work we may investigate counter-example guided abstraction refinement. We would need counter-examples from the models of the existential
Presburger formula, and refinement techniques to add counters and reversals aswell as predicates. Furthermore, as we allow user defined numerical constraints
on reachability, we may also restrict LTL model checking to runs satisfying additional numerical fairness constraints.
Acknowledgments. We thank the authors of [7] and [33] for their correspondence, V. D’Silva for recommending [21], J. Leroux and P. Ruemmer for suggesting Z3, A. Sangnier for [13], and anonymous referees for their comments. We
thank EPSRC (EP/F036361 and EP/H026878/1) for their support.

References
1. R. Alur and D. L. Dill. A Theory of Timed Automata. Theor. Comput. Sci.,
126(2):183–235, 1994.
2. T. Ball, B. Cook, V. Levin and S. K. Rajamani. SLAM and Static Driver Verifier:Technology Transfer of Formal Methods inside Microsoft. In IFM’04, pages 1–20.
3. T. Ball and S. K. Rajamani. Bebop: A Symbolic Model Checker for Boolean
Programs. In SPIN’00, pages 113–130.
4. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR’97, pages 135–150.
5. P. Bouyer. Model-checking timed temporal logics. Electr. Notes Theor. Comput.
Sci., 231:323–341, 2009.
6. T. Cachat. Uniform Solution of Parity Games on Prefix-Recognizable Graphs.
Electr. Notes Theor. Comput. Sci., 68(6), 2002.
1

Comparison with constants is not implemented. We adjusted the formula by hand.

16

Matthew Hague and Anthony Widjaja Lin

7. R. Chadha, A. Legay, P. Prabhakar and M. Viswanathan. Complexity Bounds for
the Verification of Real-Time Software. In VMCAI’10, pages 95–111.
8. C. Courcoubetis and M. Yannakakis. Minimum and Maximum Delay Problems in
Real-Time Systems. FMSD, 1(4):385–415, 1992.
9. Z. Dang et al. Binary Reachability Analysis of Discrete Pushdown Timed Automata. In CAV’00, pages 69–84.
10. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.
11. V. D’Silva, D. Kroening and G. Weissenbacher. A Survey of Automated Techniques
for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits andSystems, 27(7):1165–1178, 2008.
12. J. Esparza, A. Kucera and S. Schwoon Model checking LTL with regular valuations
for pushdown systems. Inf. Comput., 186(2):355–376, 2003.
13. E. Filiot, J.-F. Raskin, P.-A. Reynier, F. Servais, and J.-M. Talbot. Properties ofvisibly pushdown transducers. In MFCS, 2010.
14. A. Finkel and A. Sangnier. Reversal-bounded counter machines revisited. In
MFCS, 2008.
15. D. Gries. The Science of Programming. Springer-Verlag, 1981.
16. E. M. Gurari and O. H. Ibarra. The Complexity of Decision Problems for FiniteTurn Multicounter Machines. J. Comput. Syst. Sci., 22(2):220–229, 1981.
17. M. Hague. Saturation Methods for Global Model-Checking Pushdown Systems. PhD
thesis, Oxford University Computing Laboratory, 2009.
18. R. Howell and L. Rosier. An Analysis of the Nonemptiness Problem for Classes ofReversal-Bounded Multicounter Machines. J. Comput. Syst. Sci., 34(1):55–74.
19. O. H. Ibarra. Reversal-Bounded Multicounter Machines and Their Decision Problems. J. ACM, 25(1):116–133, 1978.
20. O. Ibarra, J. Su, Z. Dang, T. Bultan, R. Kemmerer. Counter machines and verification problems. Theor. Comput. Sci. 289 (2002), 165–189.
21. R. Jhala and K. L. McMillan. A practical and complete approach to predicate
refinement. In TACAS, 2006.
22. F. Laroussinie, A. Meyer, E. Petonnet. Counting CTL. In FoSSaCS’10, p. 206–220.
23. C. H. Papadimitriou and K. Steiglitz. Combinatorial Optimization: Algorithms
and Complexity. Dover Publications, 1998.
24. R. Parikh. On context-free languages. J. ACM, 13(4):570–581, 1966.
25. A.
Patterson.
PCI:
fix
memoryleakinaer inject.
https://patchwork.kernel.org/patch/53058/, 2003.
26. B. Scarpellini. Complexity of Subcases of Presburger Arithmetic. Trans. of AMS,
284(1):203–218, 1984.
27. M. Sipser. Introduction to the Theory of Computation. PWS Publishing Co., 1997.
28. A. P. Sistla and E. M. Clarke. The Complexity of Propositional Linear Temporal
Logics. J. ACM 32(3):733–749 (1985)
29. D. Suwimonteerabuth, S. Schwoon and J. Esparza. jMoped: A Java Bytecode
Checker Based on Moped. In TACAS’05, pages 541–545.
30. J. Thornbur.
dm: Fix memory leak in dm register target().
http://lkml.org/lkml/2003/6/9/70, 2003.
31. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches.
PhD thesis, School of Informatics, University of Edinburgh, 2010.
32. M. Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic
Program Verification. In LICS’86, pages 332–344.
33. H. Veith. Languages Represented by Boolean Formulas. Inf. Process. Lett.,
63(5):251–256, 1997.
34. K. N. Verma, H. Seidl and T. Schwentick. On the Complexity of Equational Horn
Clauses. In CADE’05, pages 337–352.
35. I. Walukiewicz. Model Checking CTL Properties of Pushdown Systems. In
FSTTCS’00, pages 127–138.