No.078 Higher-Order Model Checking

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.

Topics:

• 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.