With the increasing importance of software reliability, program verification has been an important and hot research topic. Recently, we have seen some good progress in automated techniques for verification of higher-order programs.
Studies of game semantics have yielded compositional model checkers and automated program equivalence checkers for Algol-like programming languages, and studies of higher-order recursion schemes and pushdown automata have yielded model checkers for higher-order functional programs. Classical control flow analysis has been recently revisited to yield more precise and/or efficient methods than Shivers’ k-CFA.

The aim of the workshop is to bring together researchers on automated techniques for higher-order program verification and analyses, and provide them with an opportunity to exchange new research results, and discuss further extensions.
The workshop also aims for cross-fertilization of different techniques for higher-order program verification, such as game semantics, type theories, higher-order grammars and pushdown systems, control flow analyses, and abstract interpretation.