Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 14:30 - 15:00 at Sala X - Session 2 Chair(s): Thomas P. Jensen

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.

Mon 14 Jan

14:00 - 15:30: PEPM 2019 - Session 2 at Sala X
Chair(s): Thomas P. JensenINRIA Rennes
pepm-2019-papers14:00 - 14:30
Sihan XuNankai University, China, Sen ZhangNankai University, China, Weijing WangNankai University, China, Xinya CaoNankai University, China, Chenkai GuoNankai University, China, Jing XuNankai University, China
pepm-2019-papers14:30 - 15:00
Keiichi WatanabeUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Hiroki OshikawaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan
pepm-2019-papers15:00 - 15:30
Gabriel RadanneUniversity of Freiburg, Germany
DOI Pre-print File Attached