[TYPES/announce] Postdoc position on automated verification of higher-order programs

[koba]

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

The appointment can start as early as September 2012 (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-350,000 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 is.s.u-tokyo.ac.jp), no later than June 30th, 2012.


Project Description
--------------------
Project Title: Higher-Order Model Checking and its Applications
Principal Investigator: Naoki Kobayashi (University of Tokyo)
Collaborators: Atushi Igarashi (Kyoto University) and Ayumi Shinohara (Tohoku University)
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, Kazutaka Matsuda, and Ayumi Shinohara
"Functional Programs as Compressed Data", PEPM 2012.

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

---------------------
Naoki Kobayashi
Department of Computer Science
Graduate School of Information Science and Technology
Univeristy of Tokyo
7-3-1 Hongo, Bunkyo-ku, Tokyo, 113-0033 Japan
email: koba at is.s.u-tokyo.ac.jp