Christopher H Broadbent
email: broadben@in.tum.de

Arnaud Carayol
email: arnaud.carayol@univ-mlv.fr

Matthew Hague
email: matthew.hague@rhul.ac.uk

Olivier Serre
email: olivier.serre@liafa.univ-paris-diderot.fr

C-SHORe

Keywords: F.1.1 [Models of Computation]: Automata Higher-Order, Verification, Model-Checking, Recursion Schemes, Collapsible Pushdown Systems

come

Introduction

Functional languages such as Haskell, OCaML and Scala strongly encourage the use of higher-order functions. This represents a challenge for software verification, which usually does not model recursion accurately, or models only first-order calls (e.g. SLAM [START_REF] Ball | The SLAM project: Debugging system software via static analysis[END_REF] and Moped [START_REF] Schwoon | Model-checking Pushdown Systems[END_REF]). However, there has recently been much interest in a model called higher-order recursion schemes (HORS) (see e.g. [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF]), which offers a way of abstracting functional programs in a manner that precisely models higher-order control-flow.

The execution trees of HORS enjoy decidable µ-calculus theories [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], which testifies to the good algorithmic properties of the model. Even 'reachability' properties (subsumed by the µ-calculus) are very useful in practice. As a simple example, the safety of incomplete pattern matching clauses could be checked by asking whether the program can 'reach a state' where a pattern match failure occurs. More complex 'reachability' properties can be expressed using a finite automaton and could, for example, specify that the program respects a certain discipline when accessing a particular resource (see [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF]). Despite even reachability being (n -1)-EXPTIME complete, recent research has revealed that useful properties of HORS can be checked in practice.

Kobayashi's TRecS [START_REF] Kobayashi | Model-checking higher-order functions[END_REF] tool, which checks properties expressible by a deterministic trivial Büchi automaton (all states accepting), was the first to achieve this. It works by determining whether a HORS is typable in an intersection-type system characterising the property to be checked [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF]. In a bid to improve scalability, a number of other algorithms have subsequently been designed and implemented such as Kobayashi et al.'s GTRecS(2) [START_REF] Kobayashi | A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes[END_REF][START_REF] Kobayashi | GTRECS2: A model checker for recursion schemes based on games and types[END_REF] and Neatherway et al.'s TravMC [START_REF] Neatherway | A traversal-based algorithm for higher-order model checking[END_REF] tools (appearing in ICFP 2012), all of which remain based on intersection type inference.

This work is the basis of various techniques for verifying functional programs. Kobayashi et al. have developed MoCHi [START_REF] Kobayashi | Predicate abstraction and cegar for higher-order model checking[END_REF] that checks safety properties of (OCaML) programs, and EHMTT Verifier [START_REF] Unno | Verification of treeprocessing programs via higher-order model checking[END_REF] for tree processing programs. Both use a model-checker for recursion schemes as a central component. Similarly, Ramsay and Ong [START_REF] Ong | Verifying higher-order functional programs with pattern-matching algebraic data types[END_REF] provide a verification procedure for programs with pattern matching employing recursion schemes as an abstraction.

Despite much progress, even the state-of-the-art TRecS does not scale to recursion schemes big enough to model realistically sized programs; achieving scalability while accurately tracking higher-order control-flow is a challenging problem. This paper of-fers an automata-theoretic perspective on this challenge, providing a fresh set of tools that contrast with previous intersection-type approaches. Techniques based on pushdown automata have previously visited ICFP, such as the approximate higher-order controlflow analysis CFA2 [START_REF] Vardoulakis | Pushdown flow analysis of first-class control[END_REF], but our aims are a bit different in that we wish to match the expressivity of HORS. Consequently we require a more sophisticated notion of pushdown automaton.

Collapsible pushdown systems (CPDS) [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] are an alternative representation of the class of execution trees that can be generated by recursion schemes (with linear-time mutual-translations between the two formalisms [START_REF] Carayol | Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection[END_REF][START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]). While pushdown systems augment a finite-state machine with a stack and provide an ideal model for first-order programs [START_REF] Jones | Even simple programs are hard to analyze[END_REF], collapsible pushdown systems model higher-order programs by extending the stack of a pushdown system to a nested "stack-of-stacks" structure. The nested stack structure enables one to represent closures. Indeed the reader might find it helpful to view a CPDS as being Krivine's Abstract Machine in a guise making it amenable to the generalisation of techniques for pushdown model-checking. Salvati and Walukiewicz have studied in detail the connection with the Krivine abstract machine [START_REF] Salvati | Recursive schemes, krivine machines, and collapsible pushdown automata[END_REF].

For ordinary ('order-1') pushdown systems, a model-checking approach called saturation has been successfully implemented by tools such as Moped [START_REF] Schwoon | Model-checking Pushdown Systems[END_REF] and PDSolver [START_REF] Hague | Analysing mu-calculus properties of pushdown systems[END_REF]. Given a regular set of configurations of the pushdown system (represented by a finite automaton A acting on stacks), saturation can solve the 'backward reachability problem' by computing another finite automaton recognising a set of configurations from which a configuration in L(A) can be reached. This is a fixed-point computation that gradually adds transitions to A until it is 'saturated'. If A recognises a set of error configurations, one can determine whether the pushdown system is 'safe' by checking if its initial configuration is recognised by the automaton computed by saturation.

We recently extended the saturation method to a backward reachability analysis of collapsible pushdown systems [START_REF] Broadbent | A saturation method for collapsible pushdown systems[END_REF]. This runs in PTIME when the number of control states is bounded. Crucially, this condition is satisfied when translating from recursion schemes of bounded arity with properties represented by automata of bounded size [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. Whilst the HORS/intersection-type based tool GTRecS(2) also enjoys this fixed-parameter tractability (others do not), it times out on many benchmarks that our tool solves quickly.

Motivated by these facts, we revisit the foundations of higherorder verification tools and introduce C-SHORe -the first modelchecking tool for the (direct) analysis of collapsible pushdown systems. Whilst the tool is based on the ICALP 2012 result, some substantial modifications and additions are made to the algorithm, leading to several novel practical and theoretical contributions:

1. An approximate forward reachability algorithm providing data (a) . . . allowing for the CPDS to be pruned so that saturation receives a smaller input.

(b) . . . employed by a modified saturation algorithm to guide its backward search.

This is essential for termination on most of our benchmarks.

2. A method for extracting witnesses to reachability.

3. A complete reworking of the saturation algorithm that speeds up the fixed-point computation.

Experimental results

showing our approach compares well with TRecS, GTRecS(2) and TravMC.

It is worth remarking that the other type-based tools mentioned above all work by propagating information in a forward direction with respect to the evaluation of the model. In contrast, the raw saturation algorithm works backwards, but we also show here how forward and backward propagation can be combined.

In Sections 5 to 8 we describe the original contributions of this paper. These sections can be understood independently of one another, and hence the reader does not need to fully grasp each section before continuing to the next. The remaining sections describe the background, related work and conclusions.

In Section 3 we recall the basic structures used in the paper as well as recapping the ICALP 2012 algorithm. In Section 5 we describe the approximate forwards-reachability analysis and how it is exploited. In Section 6 we show how to generate witnesses to reachability. In Section 7, we then consider how to restructure the saturation algorithm to more efficiently compute the fixed-point. We provide experimental results in Section 8. Note that we do not discuss in formal detail the translation from HORS model-checking to reachability for CPDS, which essentially follows [START_REF] Carayol | Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection[END_REF]. However, we do give an informal overview in Section 2, which we hope serves to demonstrate how closures can be accurately modelled.

The tool is available at http://cshore.cs.rhul.ac.uk. An appendix containing additional material appears in the long version of this paper, available from the same URL.

Modelling Higher-Order Programs

In this section we give an informal introduction to the process of modelling higher-order programs for verification. In particular, we show how a simple example program can be modelled using a higher-order recursion scheme, and then we show how this scheme is evaluated using a collapsible pushdown system. For a more systematic approach to modelling higher-order programs with recursion schemes, we refer the reader to work by Kobayashi et al. [27]. This section is for background only, and can be safely skipped.

For this section, consider the toy example below.

Main = MakeReport Nil MakeReport x = if * (Commit x) else (AddData x MakeReport) AddData y f = if * (f Error) else (f Cons(_, y))
In this example, * represents a non-deterministic choice (that may, for example, be a result of some input by the user). Execution begins at the Main function whose aim is to make a report which is a list. We begin with an empty report and send it to MakeReport. Either MakeReport indicates the report is finished and commits the report somehow, or it adds an item to the head of the list, using the AddData function, which takes the report so far, and a continuation. AddData either detects a problem with the new data (maybe it is inconsistent with the rest of the report) and flags an error by passing Error to the continuation, or extends the report with some item. In this case, the programmer has not provided error handling as part of the MakeReport function, and so an Error may be committed.

Higher-Order Recursion Schemes

As a first step in modelling this program, we introduce, informally, higher-order recursion schemes. These are rewrite systems that generate the computation tree of a functional program. A rewrite rule takes the form

N φ x ֒→ t
where N is a typed non-terminal with (possibly higher-order) arguments φ and x. A term N t φ tx rewrites to t with t φ substituted for φ and tx substituted for x. Note that recursion schemes require t to be of ground type. We will illustrate the behaviour of a recursion scheme and its use in analysis using the toy example from above.

We can directly model our example with the scheme

main ֒→ M nil M x ֒→ or (commit x) (A x M ) A y φ ֒→ or (φ error) (φ (cons y))
where M is the non-terminal associated with the MakeReport function, and A is the non-terminal associated with the AddData function; nil, or, commit, error and cons are terminal symbols of arity 0, 2, 1, 0 and 1 respectively (e.g. in the second rule, or takes the two arguments (commit x) and (A x M )). The scheme above begins with the non-terminal main and, through a sequence of rewrite steps, generates a tree representation of the evolution of the program. Figure 1, described below, shows such a sequence. Beginning with the non-terminal main, we apply the first rewrite rule to obtain the tree representing the term (A nil). We then apply the second rewrite rule, instantiating x with nil to obtain the next tree in the sequence. This continues ad infinitum to produce a possibly infinite tree labelled only by terminals.

We are interested in ensuring the correctness of the program. In our case, this means ensuring that the program never attempts to commit an error. By inspecting the rightmost tree in Figure 1, we can identify a branch labelled or, or, or, commit, error. This is an error situation because commit is being called with an error report. In general we can define the regular language Lerr = or * commit or * error. If the tree generated by the recursion scheme contains a branch labelled by a word appearing in Lerr, then we have identified an error in the program.

Collapsible Pushdown Automata

Previous research into the verification of recursion schemes has used an approach based on intersection types (e.g. [START_REF] Kobayashi | Higher-order model checking: From theory to practice[END_REF][START_REF] Neatherway | A traversal-based algorithm for higher-order model checking[END_REF]). In this work we investigate a radically different approach exploiting the connection between higher-order recursion schemes and an automata model called collapsible pushdown automata (CPDA). These two formalisms are, in fact, equivalent.

Theorem 2.1 (Equi-expressivity [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]). For each order-n recursion scheme, there is an order-n collapsible pushdown automaton generating the same tree, and vice-versa. Furthermore, the translations in both directions are linear.

We describe at a high level the structure of a CPDA and how they can be used to evaluate recursion schemes. In our case, this means outputting a sequence of non-terminals representing each path in the tree. More formal definitions are given in Section 3. At any moment, a CPDA is in a configuration p, w , where p is a control state taken from a finite set P, and w is a higherorder collapsible stack. In the following we will focus on the stack. Control states are only needed to ensure that sequences of stack operations occur in the correct order and are thus elided for clarity.

In the case of our toy example, we have an order-2 recursion scheme and hence an order-2 stack. An order-1 stack is a stack of characters a from a finite alphabet Σ. An order-2 stack is a stack of order-1 stacks. Thus we can write [[main]] to denote the order-2 stack containing only the order-1 stack [main]; [main] is an order-1 stack containing only the character main. In general Σ will contain all subterms appearing in the original statement of our toy example recursion scheme. The evolution of the CPDA stack is given in Figure 2 and explained below.

The first step is to rewrite main using main ֒→ M nil. Since (M nil) is a subterm of our recursion scheme, we have (M nil) ∈ Σ and we simply rewrite the stack

[[main]] to [[M nil]].
The next step is to call the function M . As is typical in the execution of programs, a function call necessitates a new stack frame. In particular, this means pushing the body of M (that is (or (commit x) (A x M ))) onto the stack, resulting in the third stack in Figure 2. Note that we do not instantiate the variable x, hence we use only the subterms appearing in the recursion scheme.

Recall that we want to obtain a CPDA that outputs a sequence of terminals representing each path in the tree. To evaluate the term or (• • • ) (• • • ) we have to output the terminal or and then (non-deterministically) choose a branch of the tree to follow. Let us choose (A x M ). Hence, the CPDA outputs the terminal or and rewrites the top term to (A x M ). Next we make a call to the A function, pushing its body on to the stack, and then pick out the (φ error) branch of the or terminal. This takes us to the beginning of the second row of Figure 2.

To proceed, we have to evaluate (φ error). To be able to do this, we have to know the value of φ. We can obtain this information by inspecting the stack and seeing that the second argument of the call of A is M . However, since we can only see the top of a stack, we would have to remove the character (φ error) to be able to determine that φ = M , thus losing our place in the computation.

This is where we use the power of order-2 stacks. An order-2 stack is able -via a push2 operation -to create a copy of its topmost order-1 stack. Hence, we perform this copy (note that the top of the stack is written on the left) and delve into the copy of the stack to ascertain the value of φ. While doing this we also create a collapse link, pictured as an arrow from M to the term (φ error). This collapse link is a pointer from M to the context in which M will be evaluated. In particular, if we need to know the value of x in the body of M , we will need to know that M was called with the error argument, within the term (φ error); the collapse link provides a pointer to this information (in other words we have encoded a closure in the stack). We can access this information via a collapse operation. These are the two main features of a higherorder collapsible stack, described formally in the next section.

To continue the execution, we push the body of M on to the stack, output the or symbol and choose the (commit x) branch. Since commit is a terminal, we output it and pick out x for evaluation. To know the value of x, we have to look into the stack and follow the collapse link from M to (φ error). Note that we do not need to create a copy of the stack here because x is an order-0 variable and thus represents a self-contained execution. Since error is the value of the argument we are considering, we pick it out and then output it before terminating. This completes the execution corresponding to the error branch identified in Figure 1.

Collapsible Pushdown Systems

The CPDA output or, or, or, commit, error in the execution above. This is an error sequence in Lerr and should be flagged. In general, we take the finite automaton A representing the regular language Lerr and form a product with the CPDA described above. This results in a CPDA that does not output any symbols, but instead keeps in its control state the progression of A. Thus we are interested in whether the CPDA is able to reach an accepting state of A, not the language it generates. We call a CPDA without output symbols a collapsible pushdown system (CPDS), and the question of whether a CPDS can reach a given state is the reachability problem. This is the subject of the remainder of the paper.

Preliminaries

Collapsible Pushdown Systems

We first introduce higher-order collapsible stacks and their operations, before giving the definition of collapsible pushdown systems.

Higher-Order Collapsible Stacks and Their Operations

Higher-order collapsible stacks are built from a stack alphabet Σ and form a nested "stack-of-stacks" structure. Using an idea from panic automata [START_REF] Knapik | Unsafe grammars and panic automata[END_REF], each stack character contains a pointercalled a "link" -to a position lower down in the stack. Operations updating stacks (defined below) may create copies of sub-stacks. The link is intuitively a pointer to the context in which the stack character was first created. In the sequel, we fix the maximal order to n, and use k to range between 1 and n. In the definition below, we defer the meaning of collapse link to Definition 3.2. The behaviour of a toy recursion scheme. Collapse links point to positions in the stack. Before describing them formally, we give an informal description and some basic definitions. An order-n stack can be represented naturally as an edgelabelled word-graph over the alphabet {[n-1, . . . , [1, ]1, . . . , ]n-1}⊎ Σ, with additional collapse-links pointing from a stack character in Σ to the beginning of the graph representing the target of the link. For technical convenience we do not use [n or ]n symbols (these appear uniquely at the beginning and end of the stack). An example order-3 stack is given in Figure 3, with only a few collapse links shown, ranging from order-3 to order-1 respectively.

[[main]] -→ [[A nil]] -→ or (commit x) (A x M ) M nil or -→ A x M M nil -→     or • • • A x M M nil     or -→     φ error A x M M nil     -→     φ error A x M M nil     φ error A x M M nil     -→   M M nil   φ error A x M M nil     -→     or • • • M M nil     φ error A x M M nil     or -→     commit x M M nil     φ error A x M M nil     commit -----→     x M M nil     φ error A x M M nil     -→     error A x M M nil     error ---→ •
Stacks are written with the top on the left. Given an order-n stack [w ℓ . . . w1]n, we define

topn+1([w ℓ . . . w1]n) = [w ℓ . . . w1]n topn([w ℓ . . . w1]n) = w ℓ if ℓ > 0 topn([ ]n) = [ ]n-1 otherwise top k ([w ℓ . . . w1]n) = top k (w ℓ ) if k < n and ℓ > 0 noting that top k (w) is undefined if top k ′ (w) is empty for any k ′ > k.
We also remove the top portion of a top k stack using

bot i n ([w ℓ . . . w1]n) = [wi . . . w1
]n when i ≤ ℓ and ℓ > 0, and

bot i k ([w ℓ . . . w1]n) = [bot i k (w ℓ )w ℓ-1 . . . w1
]n when k < n and ℓ > 0. We are now ready to define collapse links.

Definition 3.2 (Collapse Links

). An order-k collapse link is a pair (k, i) where 1 ≤ k ≤ n and i > 0.

For top1(w) = a where a has the link (k, i), the destination of the link is bot i k (w). We disallow collapse links where bot i k does not lead to a valid stack. The example stack in Figure 3 is thus [[[a (3,1) b]1]2[[c (2,1) ]1[d (1,1) e]1]2]3, where collapse links are denoted as superscripts. Often (as we have done for the stack characters b and e) we will omit these superscripts for readability.

Finally the following notation appends a stack on top of another. Given an order-k stack

v = [v ℓ . . . v1] k and an order-(k ′ -1) stack u (with k ′ ≤ k), we define u : k ′ v = [u v ℓ . . . v1] k if k ′ = k and u : k ′ v = [(u : k ′ v ℓ ) . . . v1] k if k ′ < k.
The following operations apply to an order-n collapsible stack.

On = {pop1, . . . , popn} ∪ {push2, . . . , pushn} ∪ {collapse2, . . . , collapsen} ∪ push 2 a , . . . , push n a , rewa | a ∈ Σ We define each stack operation for an order-n stack w. Collapse links are created by push k a , which add a character to the top of a given stack w with a link pointing to top k+1 (pop k (w)). This gives a access to the context in which it was created. We set

1. pop k (u : k v) = v, 2. push k (u : k v) = u : k (u : k v), 3. collapse k (w) = bot i k (w) where top1(w) = a (k,i) for some i, 4. push k b (w) = b (k,ℓ-1) :1 w where top k+1 (w) = [w ℓ . . . w1] k , 5. rew b a (k,i) :1 v = b (k,i) :1 v.
Note that, for a push k operation, links outside of u = top k (w) point to the same destination in both copies of u, while links pointing within u point within the respective copies of u. Since collapse1 would always be equivalent to pop1, we neither create nor follow order-1 links. (Often in examples we do not illustrate links that are never used.) For a more detailed introduction see [START_REF] Carayol | Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection[END_REF].

Collapsible Pushdown Systems

We are now ready to define collapsible pushdown systems.

Definition 3.3 (Collapsible Pushdown Systems

). An order-n collapsible pushdown system (n-CPDS) is a tuple C = (P, Σ, R) where P is a finite set of control states, Σ is a finite stack alphabet, and R ⊆ P × Σ × On × P is a set of rules.

A configuration of a CPDS is a pair p, w where p ∈ P and w ∈ Stacksn. We denote by p, w -→ p ′ , w ′ a transition from a rule (p, a, o, p ′ ) with top1(w) = a and w

′ = o(w). A run of a CPDS is a finite sequence p0, w0 -→ • • • -→ p ℓ , w ℓ . • • • • • • • • • • • • • • • • [2 [1 a b ]1 ]2 [2 [1 c ]1 [1 d e ]1 ] 2
Figure 3: A graph representation of a stack.

Representing Sets of Stacks

Our algorithm represents sets of configurations using order-n stack automata. These are a kind of alternating automata with a nested structure that mimics the nesting in a higher-order collapsible stack. We recall the definition below.

Definition 3.4 (Order-n Stack Automata). An order-n stack automaton A = (Qn, . . . , Q1, Σ, ∆n, . . . , ∆1, Fn, . . . , F1) is a tuple where Σ is a finite stack alphabet, and

1. for all n ≥ k ≥ 2, we have Q k is a finite set of states, F k ⊆ Q k is a set of accepting states, and ∆ k ⊆ Q k × Q k-1 × 2 Q k is a
transition relation such that for all q and Q there is at most one q ′ with (q, q ′ , Q) ∈ ∆ k , and 2. Q1 is a finite set of states, F1 ⊆ Q1 a set of accepting states, and

∆1 ⊆ 2≤k≤n Q1 × Σ × 2 Q k × 2 Q 1 a transition rela- tion.
The sets Q k are disjoint and their states recognise orderk stacks. Stacks are read from "top to bottom". A transition

(q, q ′ , Q) ∈ ∆ k , written q q ′ -→ Q, from q to Q for some k > 1 requires that the top k-1 stack is accepted from q ′ ∈ Q (k-1)
and the rest of the stack is accepted from each state in Q. At order-1, a transition (q, a, Q col , Q) has the additional requirement that the stack linked to by a is accepted from Q col . A stack is accepted if a subset of F k is reached at the end of each order-k stack. We write w ∈ Lq(A) to denote the set of all w accepted from q. Note that a transition to the empty set is distinct from having no transition. Figure 4 shows part of a run over the stack in Figure 3 where each node in the graph is labelled by the states from which the remainder of the stack containing it (as well as the stacks linked to) must be accepted. Note, e.g., that since Q2 appears at the bottom of an order-2 stack, we must have Q2 ⊆ F2 for the run to be accepting. The transitions used are q3

q 2 -→ Q3 ∈ ∆3, q2 q 1 -→ Q2 ∈ ∆2, and q1 a ---→ Q col Q1 ∈ ∆1. See Section 4 for further examples. q3 q2 q1 Q1 • • • Q2 Q3 ∪ Q col • • • [2 [1 a b ]1 ]2 [2

Representing Transitions and States

We use a long-form notation (defined below) that captures nested sequences of transitions. For example, we may write q3

a ---→ Q col (Q1, Q2, Q3
) to capture the transitions shown in Figure 4. Together, these indicate that after starting from the beginning of the stack and reading only the topmost stack character, the remainder of the stack must be accepted by Q col , Q1, Q2, and Q3. More generally, we may also use q3 -→ (Q2, Q3), and q3

q 2 -→ (Q3). Formally, when q ∈ Q k , q ′ ∈ Q k ′ , Qi ⊆ Qi for all k ≥ i ≥ 1,
and there is some i with Q col ⊆ Qi, we write

q a ---→ Q col (Q1, . . . , Q k ) and q q ′ -→ (Q k ′ +1 , . . . , Q k ) .
In the first case, there exist q k-1 , . . . , q1 such that q

q k-1 ---→ Q k ∈ ∆ k , q k-1 q k-2 ---→ Q k-1 ∈ ∆ k-1 , . . . , q1 a ---→ Q col Q1 ∈ ∆1.
In the second case there exist q k-1 , . . . , q k ′ +1 with q

q k-1 ---→ Q k ∈ ∆ k , q k-1 q k-2 ---→ Q k-1 ∈ ∆ k-1 , . . . , q k ′ +2 q k ′ +1 ----→ Q k ′ +2 ∈ ∆ k ′ +2 and q k ′ +1 q ′ -→ Q k ′ +1 ∈ ∆ k ′ +1 .
Remark 3.1. We may also write qQ k ,...,Q k ′ +1 for the q ′ above (which is uniquely determined by Q k , . . . , Q k ′ +1 ).

Note that our definitions mean that we have, e.g., q a ---→

Q col (Q1, Q2, Q3) if and only if we have qQ 3 ,Q 2 a ---→ Q col Q1 in ∆1.

Representing Sets of Transitions

Let ∆ S k denote the set of all order-k long-form transitions q a ---→

Q col (Q1, . . . , Q k ) of order-k. For a set T = {t1, . . . , t ℓ } ⊆ ∆ S k , we say T is of the form Q a ---→ Q col (Q1, . . . , Q k ) whenever Q = {q1, . . . , q ℓ } and for all 1 ≤ i ≤ ℓ we have ti = qi a ---→ Q i col Q i 1 , . . . , Q i k and Q col = 1≤i≤ℓ Q i col and for all 1 ≤ k ′ ≤ k, Q k ′ = 1≤i≤ℓ Q i k ′ .
Because a link can only be of one order, we insist that

Q col ⊆ Q k ′ for some 1 ≤ k ′ ≤ n.

Representing Sets of Configurations

We define a notion of P-multi-automata [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] for representing sets of configurations of collapsible pushdown systems. Definition 3.5 (P-Multi Stack Automata). Given an order-n CPDS with control states P, a P-multi stack automaton is an ordern stack automaton A = (Qn, . . . , Q1, Σ, ∆n, . . . , ∆1, Fn, . . . , F1) such that for each p ∈ P there exists a state qp ∈ Qn.

A state is initial if it is of the form qp ∈ Qn for some control state p or if it is a state q k ∈ Q k for k < n such that there exists a transition q k+1 q k -→ Q k+1 in ∆ k+1 . The language of a P-multi stack automaton A is the set L(A) = p, w w ∈ Lq p (A) .

Basic Saturation Algorithm

Our algorithm computes the set P re * C (A0) of a collapsible pushdown system C and a P-multi stack automaton A0. We assume without loss of generality that initial states of A0 do not have incoming transitions and are not final. To accept empty stacks from initial states, a bottom-of-stack symbol can be used.

Let P re * C (A0) be the smallest set with P re * C (A0) ⊇ L(A0), and

P re * C (A0) ⊇ { p, w | ∃ p, w -→ p ′ , w ′ ∈ P re * C (A0) }.
We begin with A0 and iterate a saturation function Π -adding new transitions to A0 -until a 'fixed point' is reached; that is, we cannot find any more transitions to add.

Notation for Adding Transitions During saturation we designate transitions qn

a ---→ Q col (Q1, .
. . , Qn) to be added to the automaton.

Recall this represents q

q n-1 ---→ Qn ∈ ∆n, qn-1 q n-2 ---→ Qn-1 ∈ ∆n-1, . . . , q1 a ---→ Q col Q1 ∈ ∆1. Hence, we first, for each n ≥ k > 1, add q k q k-1 ---→ Q k to ∆ k if it does not already exist. Then, we add q1 a ---→ Q col Q1 to ∆1.
Justified Transitions In this paper, we extend the saturation function to add justifications to new transitions that indicate the provenance of each new transition. This permits counter example gen-eration. To each t = q a ---→ Q col (Q1, . . . , Qn) we will define the justification J(t) to be either 0 (indicating the transition is in A0), a pair (r, i), a tuple (r, t ′ , i) or a tuple (r, t ′ , T, i) where r is a rule of the CPDS, i is the number of iterations of the saturation function required to introduce the transition, t ′ is a long-form transition and T is a set of such transitions. This information will be used in Section 6 for generating counter examples. Note that we apply J to the long-form notation. In reality, we associate each justification with the unique order-1 transition q1 a ---→

Q col Q1 associated to each t.
The Saturation Function We are now ready to recall the saturation function Π for a given C = (P, Σ, R). As described above, we apply this function to A0 until a fixed point is reached. First set J(t) = 0 for all transitions of A0. The intuition behind the saturation rules can be quickly understood via a rewrite rule (p, a, rew b , p ′ ) which leads to the addition of a transition qp a ---→ Q col (Q1, . . . , Qn) whenever there already existed a transi-

tion q p ′ b ---→ Q col (Q1, . . . , Qn).
Because the rewrite can change the control state from p to p ′ and the top character from a to b, we must have an accepting run from qp with a on top whenever we had an accepting run from q p ′ with b on top. We give examples and intuition of the more complex steps in Section 4, which may be read alongside the definition below.

Definition 3.6 (The Saturation Function Π). Given an order-n stack automaton Ai we define Ai+1 = Π(Ai). The state-sets of Ai+1 are defined implicitly by the transitions which are those in Ai plus, for each r = (p, a, o, p ′ ) ∈ R,

1. when o = pop k , for each q p ′ q k -→ (Q k+1 , . . . , Qn) in Ai, add t = qp a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , .
. . , Qn) to Ai+1 and set J(t) = (r, i + 1) whenever t is not already in Ai+1, 2. when o = push k , for each t = q p ′ a ---→

Q col (Q1, . . . , Q k , . . . , Qn) and T of the form Q k a ---→ Q ′ col (Q ′ 1 , . . . , Q ′ k ) in Ai, add to Ai+1 the transition t ′ = qp a -------→ Q col ∪Q ′ col   Q1 ∪ Q ′ 1 , . . . , Q k-1 ∪ Q ′ k-1 , Q ′ k , Q k+1 , . . . , Qn   and set J(t ′ ) = (r, t, T, i + 1) if t ′ is not already in Ai+1, 3. when o = collapse k , when k = n, add t = qp a ----→ {q p ′ } (∅, . . . , ∅) if it does not exist, and when k < n, for each transition q p ′ q k -→ (Q k+1 , . . . , Qn) in Ai, add to Ai+1 the transition t = qp a ---→ {q k } (∅, . . . , ∅, Q k+1 , . . . , Qn) if t does not already exist. In all cases, if t is added, set J(t) = (r, i + 1), 4. when o = push k b for all transitions t = q p ′ b ---→ Q col (Q1, . . . , Qn) and T = Q1 a ---→ Q ′ col Q ′ 1 in Ai with Q col ⊆ Q k , add to Ai+1 the transition t ′ = qp a ---→ Q ′ col Q ′ 1 , Q2, . . . , Q k ∪ Q col , . . . , Qn ,
and set J(t ′ ) = (r, t, T, i + 1) if t ′ is not already in Ai+1,

5. when o = rew b for each transition t = q p ′ b ---→ Q col (Q1, . . . , Qn) in Ai, add to Ai+1 the transition t ′ = qp a ---→ Q col (Q1, . . . , Qn),
setting J(t ′ ) = (r, t, i) when t ′ is not already in Ai+1.

From A0, we iterate Ai+1 = Π(Ai) until Ai+1 = Ai. Generally, we terminate in n-EXPTIME. When A0 satisfies a "nonalternating" property (e.g. when we're only interested in reaching a designated control state), we can restrict Π to only add transitions where Qn has at most one element, giving (n-1)-EXPTIME complexity. In all cases saturation is linear in the size of Σ.

Examples of Saturation

As an example of saturation, consider a CPDS with the run (

p1, [b] [c] [d] push 2 a ----→ p2, [ab] [c] [d] push 2 ----→ p3, [ab] [ab] [c] [d] collapse 2 ------→ p4, [c] [d] pop 2 ---→ p5, [d] .
) qp 5 q1 ∅ ∅ [1 d ]1 (2) qp 4 q2 ∅ {qp 5 } q1 ∅ ∅ [1 c ]1 [1 d ]1 (3) qp 3 q3 ∅ ∅ ∅ ∅ ∅ ∅ {qp 4 } q2 ∅ {qp 5 } q1 ∅ ∅ [1 a b ]1 [1 a b ]1 [1 c ]1 [1 d ]1 (4) qp 2 q4 ∅ ∅ {qp 4 } q2 ∅ {qp 5 } q1 ∅ ∅ [1 a b ]1 [1 c ]1 [1 d ]1 (5) qp 1 q5 ∅ {qp 4 } q2 ∅ {qp 5 } q1 ∅ ∅ [1 b ]1 [1 c ]1 [1 d ]1 1
Figure 5: A sequence of saturation steps.

Initial Forward Analysis

In this section we distinguish an error state perr and we are interested only in whether C can reach a configuration of the form perr , w (hence our A0 is "non-alternating"). This suffices to capture the same safety (reachability) properties of recursion schemes as TRecS. We fix a stack-automaton E recognising all error configurations (those with the state perr ). We write P ost * C for the set of configurations reachable by C from the initial configuration. This set cannot be represented precisely by a stack automaton [START_REF] Bouajjani | Symbolic Reachability Analysis of Higher-Order Context-Free Processes[END_REF] (for instance using push2, we can create

[[a n ]1[a n ]1]2 from [[a n ]1]2
for any n ≥ 0). We summarise our approach then give details in Sections 5.1, 5.2 and 5.3.

It is generally completely impractical to compute P re * C (E) in full (most non-trivial examples considered in our experiments would time-out). For our saturation algorithm to be usable in practice, it is therefore essential that the search space is restricted, which we achieve by means of an initial forward analysis of the CPDS. Ideally we would compute only P re * C (E) ∩ P ost * C . Since this cannot be represented by an automaton, we instead compute a sufficient approximation T (ideally a strict subset of P re * C (E)) where: P re * C (E) ∩ P ost * C ⊆ T ⊆ P re * C (E). The initial configuration will belong to T iff it can reach a configuration recognised by E. Computing such a T is much more feasible.

We first compute an over-approximation of P ost * C . For this we use a summary algorithm [START_REF] Sharir | Two approaches to interprocedural data flow analysis[END_REF] (that happens to be precise at order-1) from which we extract an over-approximation of the set of CPDS rules that may be used on a run to perr . Let C ′ be the (smaller) CPDS containing only these rules. That is, we remove all rules that we know cannot appear on a run to perr . We could thus take T = P re * C ′ (E) (computable by saturation for C ′ ) since it satisfies the conditions above. This is what we meant by 'pruning' the CPDS (1a in the list on page 2) However, we further improve performance by computing an even smaller T (1b in the list on page 2). We extract contextual information from our over-approximation of P ost * C about how pops and collapses might be used during a run to perr . Our C ′ is then restricted to a model C ′′ that 'guards' its rules by these contextual constraints. Taking T = P re * C ′′ (E) we have a T smaller than P re * C ′ (E), but still satisfying our sufficient conditions. In fact, C ′′ will be a 'guarded CPDS' (defined in the next subsection). We cannot compute P re * C ′′ (E) precisely for a guarded CPDS, but we can adjust saturation to compute T such that P re * C ′′ (E) ⊆ T ⊆ P re * C ′ (E). This set will thus also satisfy our sufficient conditions.

Guarded Destruction

An order-n guarded CPDS (n-GCPDS) is an n-CPDS where conventional pop k and collapse k operations are replaced by guarded operations of the form pop S k and collapse S k where S ⊆ Σ. These operations may only be fired if the resulting stack has a member of

S on top. That is, for o ∈ {collapse k , pop k | 1 ≤ k ≤ n }: o S (u) := o(u) if o(u) defined and top1(o(u)) ∈ S undefined otherwise .
Note, we do not guard the other stack operations since these themselves guarantee the symbol on top of the new stack (e.g. when a transition (p, a, push2, p ′ ) fires it must always result in a stack with a on top, and (p, a, push b k , p ′ ) produces a stack with b on top). Given a GCPDS C, we write Triv(C) for the ordinary CPDS that is the trivialisation of C, obtained by replacing each pop S k (resp. collapse S k ) in the rules of C with pop k (resp. collapse k ). We modify the saturation algorithm to use 'guarded' saturation steps for pop and collapse rules. Other saturation steps are unchanged. Non-trivial guards reduce the size of the stack-automaton constructed by avoiding certain additions that are only relevant for unreachable (and hence uninteresting) configurations in the preimage. This thus improves performance. Remark 5.2. The above modification to the naive saturation algorithm can also be easily incorporated into the efficient fixed point algorithm described in Section 7.

Approximate Reachability Graphs

We now give an overview of the summary algorithm used to obtain an over-approximation of P ost * C and thus compute the GCPDS C ′′ mentioned previously. We refer the reader to the long version of this paper for details, including a formal account of the invariants on the graph maintained by the algorithm. For simplicity, we assume that a stack symbol uniquely determines the order of any link that it emits (which is the case for a CPDS obtained from a HORS).

An approximate reachability graph for C is a structure (H, E) describing an over-approximation of the reachable configurations of C. The set of nodes of the graph H consists of heads of the CPDS, where a head is a pair (p, a) ∈ P × Σ and describes configurations of the form p, u where top1(u) = a. The set E contains directed edges ((p, a), r, (p ′ , a ′ )) labelled by rules of C. Such edges over-approximate the transitions that C might make using a rule r from a configuration described by (p, a) to one described by (p ′ , a ′ ). For example, suppose that C is order-2 and has, amongst others, the rules r1 := (p1, b, push2, p2), r2 := (p2, b, push 2 c , p3) and r3 := (p3, c, pop1, p4) so that it can perform transitions:

p1, b a r 1 --→ p2, b a b a r 2 --→ p3,     c b a     b a     r 3 --→ p4,     b a     b a    
where the first configuration mentioned here is reachable. We should then have edges ((p1, b), r1, (p2, b)), ((p2, b), r2, (p3, c)) and ((p3, c), r3, (p4, b)) in E. We denote the configurations above C1, C2, C3 and C4 respectively, with respective stacks s1, s2, s3, s4. Such a graph can be computed using an approximate summary algorithm, which builds up an object (H, E, B, U ) consisting of an approximate reachability graph together with two additional components. B is a map assigning each head h in the graph a set B(h) of stack descriptors, which are (n + 1)-tuples (hn, . . . , h1, hc) of heads. In the following, we refer to h k as the order-k component and hc the collapse component. Roughly speaking, h k describes at which head the new top k -stack resulting from a pop k operation (applied to a configuration with head h) may have been created, and hc does likewise for a collapse operation. (We will use ⊥ in place of a head to indicate when pop k or collapse is undefined.) Consider C3 = p3, s3 from the example above. This has control-state p3 and top stack symbol c and so is associated with the head (p3, c). Thus B((p3,c)) should contain the stack-descriptor ((p1, b), (p2, b), (p1, b)), which describes s3. The first (order-2) component is because top2(s3) was created by a push2 operation from a configuration with head (p1, b). The second (order-1) component is because the top symbol was created via an order-1 push from (p2, b). Finally, the order-2 link from the top of s3 points to a stack occurring on top of a configuration at the head (p1, b), giving rise to the final (collapse) component describing the collapse link.

Tracking this information allows the summary algorithm to process the rule r3 to obtain a description of C4 from the description of C3. Since this rule performs a pop1, it can look at the order-1 component of the stack descriptor to see the head (p2, b), telling us that pop1 results in b being on top of the stack. Since the rule r3 moves into control-state p4, this tells us that the new head should be (p4, b). It also tells us that certain pieces of information in B((p2, b)) are relevant to the description of top2(s4) contained in B((p4, b)). First remark that this situation only occurs for the pop k and collapse k operations. To keep track of these correlations, we use the component U of the graph.

The component U is a set of approximate higher-order summary edges. A summary edge describes how information contained in stack descriptors should be shared between heads. An orderk summary edge from a head h to a head h ′ is a triple of the form (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) where each h ′ i is a head. Such a summary edge is added when processing either a pop k or a collapse k operation on an order-k link. Intuitively such a summary edge means that if (hn, . . . , h k+1 , h k , . . . , h1, hc) ∈ B(h), then we should also have (h ′ n , . . . , h ′ k+1 , h k , . . . , h1, hc) ∈ B(h ′ ). To continue our example, the r3 rule (which performs a pop1 operation) from C3 to C4 means U should contain an order-1 summary edge ((p2, b), ((p1, b)) , (p4, b)). Since pop1 is an order-1 operation, we have pop2(s3) = pop2(s4). Hence (p1, b) (the order-2 component of the stack descriptor for s3) should also be the first component of a stack descriptor for s4. However, since top1(s4) was created at a configuration with head (p2, b), the order-1 and collapse components of such a stack descriptor for s4 should be inherited from a stack descriptor in B((p2, b)). In general if we go from a configuration (p, s) with h to a configuration (p ′ , s ′ ) with head h ′ by the pop k operation or collapse k on an order-k link, we have that pop k+1 (s) = pop k+1 (s ′ ) and hence we have a summary edge (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) The construction of the approximate reachability graph is described in algorithms 1, 2, 3 and 4. The main work is done in the function ProcessHeadWithDescriptor. In particular, this is where summary edges are added for the pop k and collapse k operations. A fully worked example is given in the long version.

Extracting the Guarded CPDA

Let G = (H, E) be an approximate reachability graph for C. Let Heads(E) be the set of heads of error configurations, i.e. Heads(E) := {(perr , a) | a ∈ Σ }. We do a simple backwards reachability computation on the finite graph G to compute the set BackRules(G), which is defined to be the smallest set satisfying:

BackRules(G) = e ∈ E e = (h, r, h ′ ) ∈ E for some h ′ ∈ Heads(E) ∪ e ∈ E e = (h, r, h ′ ) ∈ E for some (h ′ , , ) ∈ BackRules(G)
The CPDS rules occurring in the triples in BackRules(G) can be used to define a pruned CPDS C ′ that reaches an error state if and only if the original also does. However, the approximate reachability graph provides enough information to construct a guarded CPDS C ′′ whose guards are non-trivial. It should be clear that the following set BackRulesG(G) of guarded rules can be computed:

                 p, a, o ′ , p ′ ( , (p, a, o, p ′ ) , ) ∈ BackRules(G) and o ′ =              o S if o is a pop or a collapse and S = b ((p, a), r, (p ′ , b)) ∈ E with r = (p, a, o, p ′ ) o if o is a rewrite or push                 
These rules define a GCPDS on which C-SHORe finally performs saturation.

Lemma 5.2. The GCPDS C ′′ defined using BackRulesG(G) satisfies:

P ost * C ∩ P re * C (E) ⊆ P re * C ′′ (E) ⊆ P re * C (E)

Algorithm 1 The Approximate Summary Algorithm

Require: An n-CPDS with rules R and heads P × Σ and initial configuration p0,

[• • • [a0]1 • • • ]n Ensure:
The creation of a structure (H, E, B, U ) where (H, E) is an approximate reachability graph and U is a set of approximate higher-order summary edges. Set H := {(p0, a0)} and set E, B and U to be empty Call AddStackDescriptor((p0, a0), (⊥, . . . , ⊥, ⊥)) return Done, (H, E, B, U ) will now be as required Algorithm 2 AddStackDescriptor(h, (hn, . . . , h1, hc))

Require: A head h ∈ H and a stack descriptor (hn, . . . , h1, hc) Ensure: (hn, . . . , h1, hc) ∈ B(h) and all additions to B(h ′ ) for all h ′ ∈ H needed to respect summary edges are made. if (hn, . . . , h1, hc) ∈ B(h) then return Done (Nothing to do) Add (hn, . . . , h1, hc) to B(h) Call ProcessHeadWithDescriptor(h, (hn, . . . , h1, hc))

for h ′ ∈ H such that (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) ∈ U do Call AddStackDescriptor(h ′ , (h ′ n , . . . , h ′ k+1 , h k , . . . , h1, hc)) return Done
Algorithm 3 ProcessHeadWithDescriptor(h, (hn, . . . , h1, hc))

Require: A head h := (p, a) ∈ H and a stack descriptor (hn, . . . , h1, hc) ∈ B(h) Ensure: All necessary modifications to the graph are made so that it is consistent with (hn, . . . , h1, hc) ∈ B(h). In particular this is the procedure that processes the CPDS rules from h (with respect to a stack described by h and the stack descriptor).

Counter Example Generation

In this section, we describe an algorithm that given a CPDS C and a stack automaton A0 such that a configuration p, w of C belongs P re * C (A0), constructs a sequence of rules of C which when applied from p, w leads to a configuration in L(A0). In practice, we use the algorithm with A0 accepting the set of all configurations starting with some error state perr. The output is a counter-example showing how the CPDS can reach this error state.

The algorithm itself is a natural one and the full details are given in the full version of this paper. We describe it informally here by means of the example in Figure 5, described in Section 4.

To construct a trace from p1,

[b] [c] [d] to p5, [d]
we first note that, when adding the initial transition of the pictured run from qp 1 , the saturation step marked that the transition was added due to the Algorithm 4 AddSummary(h, (h ′ n , . . . , h k+1 ) , h ′ ) Require: An approximate higher-order summary edge (h, (h ′ n , . . . , h k+1 ) , h ′ ) Ensure: (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) ∈ U and that all necessary stack descriptors are added to the appropriate B(h ′′ ) for h ′′ ∈ H so that all summary edges (including the new one) are respected.

if (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) ∈ U then return Done (Nothing to do) Add (h, (h ′ n , . . . , h ′ k+1 ) , h ′ ) to U for (hn, . . . , h k+1 , h k , . . . , h1, hc) ∈ B(h) do AddStackDescriptor(h ′ , (h ′ n , . . . , h ′ k+1 , h k , . . . , h1, hc)) return Done rule p1, b, push 2 a , p2 . If we apply this rule to p1, [b] [c] [d] we obtain p2, [ab] [c] [d]
(collapse links omitted). Furthermore, the justifications added during the saturation step tell us which transitions to use to construct the pictured run from qp 2 . Hence, we have completed the first step of counter example extraction and moved one step closer to the target configuration. To continue, we consider the initial transition of the run from qp 2 . Again, the justifications added during saturation tell us which CPDS rule to apply and which stack automaton transitions to use to build an accepting run of the next configuration. Thus, we follow the justifications back to a run of A0, constructing a complete trace on the way.

The main technical difficulty lies in proving that the reasoning outlined above leads to a terminating algorithm. For example, we need to prove that following the justifications does not result us following a loop indefinitely. Since the stack may shrink and grow during a run, this is a non-trivial property. To prove it, we require a subtle relation on runs over higher-order collapsible stacks.

A Well-Founded Relation on Stack Automaton Runs

We aim to define a well-founded relation over runs of the stack automaton A constructed by saturation from C and A0. To do this we represent a run over a stack as another stack of (sets of) transitions of A. This can be obtained by replacing each instance of a stack character with the set of order-1 transitions that read it. This is formally defined in the full version of the paper and described by example here. Consider the run over -→ {qp 4 } (and similarly for the transitions from qp 4 and qp 5 ) we do not need to explicitly store these transitions in our stack representation of runs.

Using this representation, we can define by induction a relation ֒→ k on the order-k runs of A. Note that this is not an order relation as it is not always transitive. There are several cases to ֒→ k .

1. For k = 1, we say w ′ ֒→1 w if for some i ≥ 0, w contains strictly fewer transitions in ∆1 justified at step i than w ′ and that for all j > i they both contain the same number of transitions in ∆1 justified at step j. It is possible to show that by following the justifications, from stack w to a w ′ , we always have w ֒→n w ′ . Since this relation is well-founded, the witness generation algorithm always terminates.

For

k > 1, we say u = [u ℓ . . . u1] k ֒→ k v = [v ℓ ′ . . . v1] k if (a) ℓ ′ < ℓ and ui = vi for i ∈ [1, ℓ ′ -1] and either u ℓ ′ = v ℓ ′ or u ℓ ′ ֒→ k-1 v ℓ ′ , or (

Efficient Fixed Point Computation

We introduce an efficient method of computing the fixed point in Section 3, inspired by Schwoon et al.'s algorithm for alternating (order-1) pushdown systems [START_REF] Suwimonteerabuth | Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains[END_REF]. Rather than checking all CPDS rules at each iteration, we fully process all consequences of each new transition at once. New transitions are kept in a set ∆new (implemented as a stack), processed, then moved to a set ∆ done , which forms the transition relation of the final stack automaton. We assume w.l.o.g. that a character's link order is determined by the character. This is true of all CPDSs obtained from HORSs.

In most cases, new transitions only depend on a single existing transition, hence processing the consequences of a new transition is straightforward. The key difficulty is the push rules, which depend on sets of existing transitions. Given a rule (p, a, push k , p ′ ), processing t = q p ′ a ---→ Q col (Q1, . . . , Q k , . . . , Qn) 'once and once only' must somehow include adding a new transition whenever there is a set of transitions of the form

Q k a ---→ Q ′ col (Q ′ 1 , . . . , Q ′ k )
in Ai either now or in the future. When t is processed, we therefore create a trip-wire, consisting of a source and target. A target collects transitions from a given set of states (such as Q k above), whilst a source describes how such a collection could be used to form a new transition according to a push saturation step. Definition 7.1. An order-k source for k ≥ 1 is defined as a tuple

(q k , q k-1 , a, Q k ) in Q k × Q ⊥ k-1 × Σ × 2 Q k where Q ⊥ 0 := {⊥} and Q ⊥ i = Qi ∪ {⊥} for i ≥ 1. An order-k target is a tuple (Q k , Q C k , Q lbl , Q ′ k ) ∈ 2 Q k × 2 Q k × 2 Q k-1 × 2 Q k if k ≥ 2, and if k = 1 (Q1, Q C 1 , a, Q col , Q ′ 1 ) ∈ n k ′ =2 2 Q 1 × 2 Q 1 × Σ × 2 Q k ′ × 2 Q 1 .
The set Q C k is a countdown containing states in Q k still awaiting a transition. We always have

Q C k ⊆ Q k and Q k \ Q C k Q lbl --→ Q ′ k . Likewise, an order-1 target (Q1, Q C 1 , a, Q col , Q1) will satisfy (Q1 \ Q C 1 ) a ---→ Q col Q ′ 1 . A target is complete if Q C k = ∅ Q C 1 = ∅.
A trip-wire of order-k is an order-k source-target pair of the form (( , , , Q k ), (Q k , , , )) when k ≥ 2 or (( , , a, Q k ), (Q k , , a, , )) when k = 1. When the target in a trip-wire is complete, the action specified by its source is triggered, which we now sketch.

An order-k source for k ≥ 2 describes how an order-(k -1) source should be created from a complete target, propagating the computation to the level below, and an order-1 source describes how a new long-form transition should be created from a complete target. That is, when we have (q k , , a, Q k ) (we hide the second component for simplicity of description) and

(Q k , ∅, Q lbl , Q ′ k ) this means we've found a set of transitions witnessing Q k Q lbl --→ Q ′ k
and should now look for transitions from Q lbl . Hence the algorithm creates a new source and target for the order-(k -1) state-set Q lbl . When this process reaches order-1, a new transition is created. This results in the construction of the t ′ from a push saturation step.

Algorithm 5 gives the main loop and introduces the global sets ∆ done and ∆new, and two arrays Usrc[k] and Utarg[k] containing sources and targets for each order. Omitted are loops processing popn and collapsen rules like the naive algorithm. Algorithm 6 gives the main steps processing a new transition. We present only two CPDS rule cases here. In most cases a new transition is created, however, for push rules we create a trip-wire. Remaining algorithms, definitions, justification handling, and proofs are given in the long version of this paper. We describe some informally below.

In create trip wire we create a trip-wire with a new target (Q k , Q k , ∅, ∅). This is added using an add target procedure which also checks ∆ done to create further targets. E.g., a new target

Q k , Q C k , Q lbl , Q ′ k combines with an existing q k q k-1 ---→ Q ′′ k to create a new target Q, Q C k \ {q k } , Q lbl ∪ {q k-1 } , Q ′ k ∪ Q ′′ k .
(This step corrects a bug in the algorithm of Schwoon et al.) Similarly update trip wires updates existing targets by new transitions. In all cases, when a source and matching complete target are created, we perform the propagations described above. Proposition 7.1. Given a CPDS C and stack automaton A0, let A be the result of Algorithm 5. We have L(A) = P re * C (A0).

Experimental Results

We compared C-SHORe with the current state-of-the-art verification tools for higher-order recursion schemes (HORS): TRecS [START_REF] Kobayashi | Model-checking higher-order functions[END_REF], GTRecS2 [START_REF] Kobayashi | GTRECS2: A model checker for recursion schemes based on games and types[END_REF] (the successor of [START_REF] Kobayashi | A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes[END_REF]), and TravMC [START_REF] Neatherway | A traversal-based algorithm for higher-order model checking[END_REF]. Benchmarks are from the TRecS and TravMC benchmark suites, plus several larger examples provided by Kobayashi. The majority of the TravMC benchmarks were translated into HORS from an extended formalism, HORS with Case statements (HORSC), using a script by Kobayashi. For fairness, all tools in our experiments took a pure HORS as input. However, the authors of TravMC report that TravMC performs faster on the original HORSC examples than on their HORS translations. In all cases, the benchmarks consist of a HORS (generating a computation tree) and a property automaton. In the case of C-SHORe, the property automaton is a regular automaton describing branches of the generated tree that are considered errors. Thus, following the intuition in Section 2, we can construct a reachability query over a CPDS, where the reachability of a control state perr indicates an erroneous branch (see [START_REF] Carayol | Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection[END_REF] for more details). All other tools check co-reachability properties of HORS and thus the property automaton describes only valid branches of the computation tree. In all cases, it was straightforward to translate between the co-reachability and reachability properties.

The experiments were run on a Dell Latitude e6320 laptop with 4Gb of RAM and four 2.7GHz Intel i7-2620M cores. We ran C-SHORe on OpenJDK 7.0 with IcedTea7 replacing binary plugs, using the argument "-Xmx" to limit RAM usage to 2.5Gb. As advised by the TravMC developers, we ran TravMC on the Mono JIT Compiler version 3.0.3 with no command line arguments. Finally TRecS (version 1.34) and GTRecS2 (version 3.17) were compiled with the OCaml version 4.00.1 compilers. On negative examples, GTRecS2 was run with its -neg argument. We used the "ulimit" command to limit memory usage to 2.5Gb and set a CPU timeout of 600 seconds (per benchmark). The given runtimes were reported by the respective tools and are the means of three separate runs on each example. Note that C-SHORe was run until the automaton was completely saturated.

Table 1 shows trials where at least one tool took over 1s. This is because virtual machine "warm-up" and HORS to CPDS conversion can skew the results on small benchmarks. Full results are in the full paper. Examples violating their property are marked "(bug)". The order (Ord) and size (Sz) of the schemes were reported by TRecS. We show reported times in seconds for TRecS (T), GTRecS2 (G), TravMC (TMC) and C-SHORe (C) where "-" means analysis failed. For C-SHORe, we report the times for HORS to CPDS translation (Ctran), CPDS analysis (Ccpds), and building the approximation graph (Capprox). Capprox is part of Ccpds, and the full time (C) is the sum of Ctran and Ccpds.

Of 26 benchmarks, C-SHORe performed best on 5 examples. In 6 cases, C-SHORe was the slowest. In particular, C-SHORe does not perform well on exp4-1 and exp4-5. These belong to a class of benchmarks that stress higher-order model-checkers and indi- cate that our tool currently does not always scale well. However, C-SHORe seems to show a more promising capacity to scale on larger HORS produced by tools such as MoCHi [START_REF] Kobayashi | Predicate abstraction and cegar for higher-order model checking[END_REF], which are particularly pertinent in that they are generated by an actual software verification tool. We also note that C-SHORe timed out on the fewest examples despite not always terminating in the fastest time.

Algorithm 5 Computing P re * C (A0) Let ∆ done = ∅, ∆new = n≥k≥1 ∆ k , Usrc[k] = ∅, Utarg[k] = {(∅, ∅, ∅, ∅)} for each n ≥ k > 1 and Utarg[1] = {(∅, ∅, a, ∅, ∅) | a ∈ Σ }. . . .
p ′ Qn•••Q k+1 --→ Q k then for p ∈ P and a ∈ Σ such that r := (p, a, pop k , p ′ ) ∈ R do add to worklist qp a ---→ Q col (∅, . . . , ∅, q p ′ Qn•••Q k+1 , Q k+1 , . . . ,
It is also very important to note that C-SHORe and GTRecS2 are the only implemented fixed-parameter tractable algorithms in the literature for HORS model-checking of which we are aware (both TRecS and TravMC have worst-case run-times nonelementary in the size of the recursion scheme). Moreover, C-SHORe generally performs much better than GTRecS2. Thus not only does C-SHORe's performance seem promising when compared to the competition, there is also theoretical reason to suggest that the approach could in principle be scalable, in contrast to some of the alternatives. Thus initial work justifies further investigation into saturation based algorithms for higher-order model-checking.

Finally, we remark that without the forwards analysis described in Section 5, all shown examples except filepath timed out. We also note that we did not implement a naive version of the saturation algorithm, where after each change to the stack automaton, each rule of the CPDS is checked for further updates. However, experi-ence implementing PDSolver [START_REF] Hague | Analysing mu-calculus properties of pushdown systems[END_REF] (for order-1 pushdown systems) indicates that the naive approach is at least an order of magnitude slower than the techniques [START_REF] Suwimonteerabuth | Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains[END_REF] we generalised in Section 7.

Related Work

The saturation technique has proved popular in the literature. It was introduced by Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] and Finkel et al. [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF] and based on a string rewriting algorithm by Benois [START_REF] Benois | Parties rationnelles du groupe libre[END_REF]. It has since been extended to Büchi games [START_REF] Cachat | Games on Pushdown Graphs and Extensions[END_REF], parity and µ-calculus conditions [START_REF] Hague | Analysing mu-calculus properties of pushdown systems[END_REF], and concurrent systems [START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF][START_REF] Suwimonteerabuth | Symbolic contextbounded analysis of multithreaded java programs[END_REF], as well as weighted pushdown systems [START_REF] Reps | Weighted pushdown systems and their application to interprocedural dataflow analysis[END_REF]. In addition to various implementations, efficient versions of these algorithms have also been developed [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Suwimonteerabuth | Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains[END_REF].

The saturation algorithm for CPDS that we introduced in [START_REF] Broadbent | A saturation method for collapsible pushdown systems[END_REF], extending and improving [START_REF] Hague | Symbolic backwards-reachability analysis for higher-order pushdown systems[END_REF] (and [START_REF] Bouajjani | Symbolic Reachability Analysis of Higher-Order Context-Free Processes[END_REF]), follows a number of papers solving parity games on the configuration graphs of higher-order automata [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF][START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Carayol | Winning Regions of Higher-Order Pushdown Games[END_REF][START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. While only handling reachability, saturation lends itself well to implementation. This paper describes such a practical incarnation and a number of significant optimisations, such as using a forwards analysis to guide the backward search. This latter point is an important way in which C-SHORe differs from previous model-checkers for HORS, which employ intersection types and propagate information purely in a forward direction. This is related to the fact that the latter accept 'co-reachability properties' (represented by trivial Büchi automata) as input, expressing the complement of properties taken by C-SHORe.

Indeed it would be interesting to investigate in more detail how approximate forward and backward analyses of varying degrees of accuracy could be combined for efficiency. It would also be helpful to more closely analyse the relationship between CPDS and typebased algorithms allowing a transfer of ideas. In any case, this paper shows that saturation-based algorithms for HORS/CPDS perform sufficiently well in practice to warrant further study.

To finish, we briefly mention several approaches to analysing higher-order programs with differing aims to ours. In static analysis, k-CFA [START_REF] Shivers | Control-Flow Analysis of Higher-Order Languages[END_REF] and CFA2 [START_REF] Vardoulakis | CFA2: Pushdown-Flow Analysis for Higher-Order Languages[END_REF] perform an over-approximative analysis of higher-order languages with at-most first-order granularity. Similarly Jhala et al. use refinement types to analyse OCaml programs by reducing the problem to first-order model-checking, which is thus incomplete [START_REF] Jhala | Hmc: Verifying functional programs using abstract interpreters[END_REF]. Finally, Hopkins et al. have produced tools for equivalence checking fragments of ML and Idealized Algol up to order-3 [START_REF] Hopkins | Homer: A higher-order observational equivalence model checker[END_REF][START_REF] Hopkins | Hector: An equivalence checker for a higher-order fragment of ml[END_REF].

Conclusion

We have considered the problem of verifying safety properties of a model that can be used to precisely capture control-flow in the presence of higher-order recursion. Whilst previous approaches to such an analysis are based on higher-order recursion schemes and intersection types, our approach is based on automata and saturation techniques previously only applied in practice to the first-order case. At a more conceptual level, our algorithm works by propagating information backwards from error states towards the initial state. Moreover, it combines this with an approximate forward analysis to gather information that guides the backward search. In contrast, the preceding type-based algorithms all work by propagating information purely in a forward direction.

Our preliminary work brings new techniques to the table for tackling a problem, which in contrast to its first-order counterpart, has proven difficult to solve in a scalable manner. Our algorithm has the advantage that it accurately models higher-order recursion whilst also being fixed-parameter tractable, therefore giving a theoretical reason for hope that it could scale. In contrast TRecS and TravMC have worst-case run-times non-elementary in the size of the recursion scheme. Our tool also seems to work significantly better in practice than GTRecS2, the only other HORS model-checker in the literature that does enjoy fixed-parameter tractability.

We therefore believe that a C-SHORe-like approach shows much promise and warrants further investigation.

Figure 1 :

 1 Figure 1: The behaviour of a toy recursion scheme.

Figure 2 :

 2 Figure 2: A stack evaluating the toy example.

Figure 4 :

 4 Figure 4: Part of a run over an example stack.

q 1

 1

Figure 5 1 -∅ 2 a-

 512 Figure 5 shows the sequence of saturation steps, beginning with an accepting run of p5, [d] and finishing with an accepting run of p1, [b] [c] [d] . The individual steps are explained below. Initial Automaton We begin at the top of Figure 5 with a stack automaton containing the transitions qp 5 q 1 -→ ∅ and q1 d -→ ∅ ∅, which

1 .Lemma 5 . 1 .

 151 when o = pop S k , for each q p ′ q k -→ (Q k+1 , . . . , Qn) in A such that there is a transition of the form q k b -→ ( , . . . , ) in A such that b ∈ S, add qp a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , . . . , Qn) to A ′ , 3. when o = collapse S k , for each q p ′ q k -→ (Q k+1 , . . . , Qn) in A such that there is a transition of the form q k b -→ ( , . . . , ) in A with b ∈ S, add qp a ---→ {q k } (∅, . . . , ∅, Q k+1 , . . . , Qn) to A ′ . E.g., suppose that an ordinary (non-guarded) 2-CPDS has rules (p1, c, collapse2, p) and (p2, d, collapse2, p ′ ). The original saturation algorithm would process these rules to add the transitions: Now suppose that the saturation algorithm has produced two transitions of the form qp a -→ ( , ) and q p ′ b -→ ( , ). If a GCPDS had, for example, the rules (p1, c, collapse {a} 2 , p) and (p2, d, collapse {b} 2 , p ′ ), then these same two transitions would be added by the modified saturation algorithm. On the other hand, the rules (p1, c, collapse {a} 2 , p) and (p2, d, collapse {a} 2 , p ′ ) would only result in the first of the two transitions being added. The revised saturation algorithm applied to E (for a GCPDS C) gives a stack automaton recognising T such that P re * C (E) ⊆ T ⊆ P re * Triv(C) (E) Remark 5.1. The algorithm may result in a stack-automaton recognising configurations that do not belong to P re * C (E) (although still in P re * Triv(C) (E)). This is because a state q k having a transition q k b -→ ( , . . . , ) may also have another transition q k b ′ -→ ( , . . . , ) with b = b ′ (and so it might recognise a stack from which a pop k , say, guarded by b cannot be performed).

  for o and p ′ such that r = (p, a, o, p ′ ) ∈ R do if o = rew b then Add (p ′ , b) to H and ((p, a), r, (p ′ , b)) to E Call AddStackDescriptor((p ′ , b), (hn, . . . , h1, hc)) else if o = push k b then Add (p ′ , b) to H and ((p, a), r, (p ′ , b)) to E Call AddStackDescriptor((p ′ , b), (hn, . . . , h2, (p, a), h k )) else if o = push k then Add (p ′ , a) to H and ((p, a), r, (p ′ , a)) to E Call AddStackDescriptor((p ′ , a), (hn, . . . , h k+1 , (p, a), h k-1 , . . . , h1, hc)) else if o = pop k with h k = (p k , a k ) where a k = ⊥ then Add (p ′ , a k ) to H and ((p, a), r, (p ′ , a k )) to E Call AddSummary((p k , a k ), (hn, . . . , h k+1 ) , (p ′ , a k )) else if o = collapse k , hc = (pc, ac) and ac = ⊥ then Add (pc, ac) to H and ((p, a), r, (p ′ , ac)) to E Call AddSummary((pc, ac), (hn, . . . , h k+1 ) , (p ′ , ac)) return Done

  [[b] [c] [d]] from qp 1 in Figure 5. We can represent this run as the stack [[{t1}] [{t2}] [{t3}]] where t1 = q5 b Note that since q5 uniquely labels the order-2 transition qp 1 q 5

  b) ℓ ′ ≥ ℓ and ui = vi for i ∈ [1, ℓ -1] and u ℓ ֒→ k-1 vi for all i ∈ [ℓ, ℓ ′ ]. Lemma 6.1. For all k ∈ [1, n], the relation ֒→ k is well-founded.Namely there is no infinite sequence w0 ֒→ k w1 ֒→ k w2 ֒→ k • • • .

  while ∃t ∈ ∆new do update rules(t); update trip wires(t); move t from ∆new to ∆ done Algorithm 6 update rules(t) if t is an order-k transition for 2 ≤ k ≤ n of the form q

Table 1 :

 1 Qn), r for p ∈ P and a ∈ Σ such that r := (p, a, push k , p ′ ) ∈ R do create trip wire qp,Q n ,...,Q k+1 , q p ′ ,Qn,...,Q k+1 ,Q k , a, Q k , (r, t) Comparison of model-checking tools. Shown in bold are the two fixed-parameter tractable algorithms, GTRecS2 and C-SHORe.

				• • •
	Benchmark file	Ord	Sz	T	TMC	G	C	Ctran Ccpds Capprox ✓/ ✗
	order5	5	52	0.007	0.039	-	0.415	0.057	0.358	0.205
	order5-2	5	40	0.022	0.084	-	0.305	0.050	0.255	0.157
	order5-variant	5	55	0.019	0.039	1.519	0.427	0.057	0.370	0.177
	filepath	2	5956 210.102	-	-	0.397	0.168	0.229	0.221	✓
	filter-nonzero (bug)	5	484	0.006	0.115	0.182	1.443	0.100	1.344	1.006	✗
	filter-nonzero-1	5	890	0.176	211.907	-	4.492	0.159	4.332	3.484
	map-head-filter-1	3	880	0.141	1.343	-	0.400	0.119	0.281	0.273
	map-plusone-1	5	459	0.030	0.736	-	1.247	0.119	1.128	0.908
	map-plusone-2	5	704	1.358	13.962	-	2.634	0.142	2.491	2.183
	exp4-1	4	31	-	0.047	0.114	-	0.039	-	0.240	✗
	exp4-5	4	55	-	-	0.818	-	0.046	-	2.128	✗
	cfa-life2	14	7648	-	-	-	-	0.479	-	-
	cfa-matrix-1	8	2944	16.937	-	-	19.230 0.332 18.898	18.892
	cfa-psdes	7	1819	17.654	-	-	1.920	0.273	1.647	1.640	✓
	dna	2	411	0.031	0.263	0.046	6.918	0.175	6.743	6.206	✗
	fibstring	4	29	-	74.569	0.114	-	0.042	-	0.256	✗
	fold fun list	7	1346	0.519	-	-	1.356	0.202	1.154	1.147
	fold right	5	1310	31.624	-	-	1.255	0.191	1.064	1.043	✓
	jwig-cal main	2	7627	0.062	0.052	0.161	3.802	3.739	0.063	0.057	✗
	l	3	35	-	15.743	0.010	0.248	0.042	0.206	0.199
	search-e-church (bug)	6	837	0.012	0.258	-	4.741	0.155	4.586	1.760
	specialize cps coerce1-c	3	2731	-	-	-	1.131	0.293	0.838	0.830	✓
	tak (bug)	8	451	-	3.945	-	41.772 0.136 41.636	34.855
	xhtmlf-div-2 (bug)	2	3003	0.234	-	39.961	2.743	2.303	0.440	0.422
	xhtmlf-m-church	2	3027	0.238	-	8.420	2.708	2.319	0.389	0.382
	zip	4	2952	22.251	-	-	3.356	0.295	3.061	1.609	✓

Acknowledgments

We are extremely to Robin Neatherway and Naoki Kobayashi for help with benchmarking, Łukasz Kaiser for web-hosting, and for discussions with Stefan Schwoon. Supported by Fond. Sci. Math. Paris, AMIS (ANR 2010 JCJC 0203 01 AMIS), FREC (ANR 2010 BLAN 0202 02 FREC), VAPF (Région IdF), and EPSRC (EP/K009907/1).