Higher-order program verification via HFL model checking

DOI10.1007/978-3-319-89884-1_25zbMath1418.68127arXiv1710.08614OpenAlexW2963426974MaRDI QIDQ2324003

Takeshi Tsukada, Keiichi Watanabe, Naoki Kobayashi

Publication date: 13 September 2019

Full work available at URL: https://arxiv.org/abs/1710.08614

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

On higher-order reachability games vs may reachability ⋮ Unnamed Item ⋮ Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking ⋮ Fold/Unfold Transformations for Fixpoint Logic

This page was built for publication: Higher-order program verification via HFL model checking