[TYPES/announce] Postdoc Position on Higher-Order Model Checking and Program Verification

[koba]

A new postdoc position is available for 5-year project "Higher-Order
Model Checking and its Applications" (see the project description below), 
at Tohoku University, Japan.

The appointment can start as early as in October 2011 (the starting date
is negotiable). The contract of appointment will be renewed for each
academic year, and can be extended up to March 2016, subject to
performance. Salary will be about 300,000 JPY (Japanese yen) per month.

Applicants should have a Ph.D in computer science or related fields,
and have a strong background in at least one (preferably two or more)
of the following topics: program verification, type systems, game
semantics, model checking, formal languages and automata, and automated 
theorem proving.

Interested candidates are invited to send a detailed CV via email to
Naoki Kobayashi (koba at ecei.tohoku.ac.jp), no later than August 15th, 2011.


Project Description
--------------------
Project Title: Higher-Order Model Checking and its Applications
Principal Investigator: Naoki Kobayashi
Project Term: June 2011 - March 2016

Model checking is one of the promising techniques for software
verification, but traditional model checking (such as finite-state and
pushdown model checking) was not suitable for verification of high-level
programs that use higher-order functions and recursion.
We have recently studied higher-order model checking (more precisely,
model checking of the trees generated by higher-order recursion
schemes, which has been studied only among theoretical communities
until recently), and shown that (i) many program verification problems
can be reduced to higher-order model checking, and that (ii) despite
its extremely high worst-case complexity, higher-order model checking
can be solved efficiently for many typical inputs. Based on those
results, we have constructed the first higher-order model checker
TRecS and implemented a prototype automated program verification tool
for a subset of ML, on top of the model checker. The aim of this
project is to further advance this series of work on higher-order
model checking and program verification, and to construct a software model
checker for full-scale functional (and possibly also object-oriented) 
programming languages. We will also exploit new applications of higher-order 
model checking, such as data compression.

Related publications:

Naoki Kobayashi, "Types and Higher-Order Recursion Schemes for
Verification of Higher-Order Programs," Proceedings of POPL 2009,
pp.416-428, 2009.

Naoki Kobayashi and Luke Ong, "A Type System Equivalent to Modal
Mu-Calculus Model Checking of Recursion Schemes," 
Proceedings of LICS 2009, pp.179-188, 2009

Naoki Kobayashi, "Model-Checking Higher-Order Functions",
Proceedings of PPDP 2009, pp.25-36, 2009.

Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno,
"Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for
 Program Verification",
Proceedings of POPL 2010, pp.495-508, 2010.

Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno,
"Predicate Abstraction and CEGAR for Higher-Order Model Checking",
Proceedings of PLDI 2011, pp.222-233, 2011.

Naoki Kobayashi, 
"Higher-Order Model Checking: From Theory to Practice",
Invited paper in Proceedings of LICS, 2010.
(A very brief survery of the field)