Name
Title | ||
|---|---|---|
Reduction from branching-time property verification of higher-order programs to HFL validity checking. |
Abstract | ||
|---|---|---|
Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In this paper, we extend Kobayashi et al.'s recent method for verification of linear-time temporal properties based on HFLZ model checking, to deal with branching-time properties. We formalize branching-time property verification problems as an extension of HORS model checking called HORSZ model checking, present a sound and complete reduction to validity checking of (modal-free) HFLZ formulas, and prove its correctness. The correctness of the reduction subsumes the decidability of HORS model checking. The HFLZ formula obtained by the reduction from a HORSZ model checking problem can be considered a kind of verification condition for the orignal model checking problem. We also discuss interactive and automated methods for discharging the verification condition.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3294032.3294077 | POPL '19: 46th Annual ACM SIGPLAN Symposium on Principles of Programming Languages
Cascais
Portugal
January, 2019 |
Keywords | DocType | ISBN |
higher-order program verification, higher-order fixpoint logic | Conference | 978-1-4503-6226-9 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Keiichi Watanabe | 1 | 4 | 1.42 |
| Takeshi Tsukada | 2 | 59 | 11.61 |
| Hiroki Oshikawa | 3 | 0 | 0.34 |
| Naoki Kobayashi | 4 | 0 | 3.38 |