Name
Abstract | ||
|---|---|---|
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-
$$n$$
programs can be reduced to may-reachability problems for order-(
$$n+1$$
) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications to higher-order program verification. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1007/978-3-031-19135-0_8 | Reachability Problems |
DocType | ISSN | Citations |
Conference | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kazuyuki Asada | 1 | 0 | 0.34 |
| Hiroyuki Katsura | 2 | 0 | 0.34 |
| Naoki Kobayashi | 3 | 0 | 3.38 |