Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Mon 2 Dec 2019 14:00 - 14:30 at Bali Room - Program Analysis Chair(s): Annabelle McIver

Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is based on Kobayashi et al.’s type-based characterization of HFL model checking, and was inspired by a saturation-based algorithm for HORS model checking, another higher-order extension of model checking. We prove the correctness of the algorithm and report on an implementation and experimental results.

Mon 2 Dec
Times are displayed in time zone: (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change

13:30 - 15:00: Research Papers - Program Analysis at Bali Room
Chair(s): Annabelle McIverMacquarie University
aplas-2019-papers13:30 - 14:00
aplas-2019-papers14:00 - 14:30
Youkichi HosoiThe University of Tokyo , Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan
aplas-2019-papers14:30 - 15:00
Tukaram MuskeTata Consultancy Services Ltd, Rohith TalluriTata Consultancy Services Ltd, Alexander SerebrenikEindhoven University of Technology