Automated Techniques for Higher-Order Program Verification

Icon

Shonan Meeting Seminar 005

Overview

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.

To participants: please leave your comments here.