Higher-Order Model Checking

Icon

NII Shonan Meeting Seminar 078

Overview

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.