Higher-Order Model Checking


NII Shonan Meeting Seminar 078


Finite state model checking has been widely studied and successfully applied to system verification. The main theme of this meeting, higher-order model checking, is a generalization of finite state model checking, obtained by replacing finite state models with more expressive models called recursion schemes.  Higher-order model checking (HOMC) has found applications in analysis of object-oriented and concurrent programs with recursion and higher-order procedures.


  • Extensions of HOMC: beyond simple types (e.g. untyped and recursively typed recursion schemes, higher-type Böhm trees); beyond omega-regular properties: finitary parity, omega-B, stack unboundedness, etc.
  • Algorithms for HOMC: HorSatZDD, Preface, C-SHORe, etc.
  • Higher-order grammars and pushdown automata: Context sensitivity of unsafe Maslov languages and other open problems.
  • Effective denotational semantics and strategy-aware models for HOMC: Compositional approaches to HOMC.

Category: Overview


Comments are closed.