[TYPES/announce] Open Postdoc Position on Higher-Order Model Checking

[koba]

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

 The appointment can start as early as April 2016 (the starting date
 is negotiable). The contract of appointment will be renewed for each
 academic year, and can be extended up to March 2020, subject to
 performance. Salary will be about 350,000-450,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 October 15th, 2015.

 Project Description
 --------------------

 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 can be considered a generalization of finite-state/pushdown
 model checking, 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 a few automated program verification tools,
 such as MoCHi, a fully-automated software model checker for a subset of OCaml.
  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 programming languages. 
 We will also exploit new applications of higher-order model checking, such as data
 compression.

 Selected publications on the topic:
 ----------------------------------
 A survey:
 * Naoki Kobayashi,
   "Higher-Order Model Checking: From Theory to Practice",
   Invited paper in Proceedings of LICS 2011.

 Theory and model checking algorithms:
 * Naoki Kobayashi, "Model Checking Higher-Order Programs," JACM, 2013.
 * Naoki Kobayashi, "Pumping by Typing," LICS 2013, pp.398-407, 2013
 * 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
 * Christopher H. Broadbent, Naoki Kobayashi,
   "Saturation-Based Model Checking of Higher-Order Recursion Schemes," 
   CSL 2013, pp.129-148, 2013

 Applications to program verification:
 * Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi,
  "Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs,"
  CAV 2015, pp.287-303, 2015

 * Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda,
  "Pairwise Reachability Analysis for Higher Order Concurrent Programs 
   by Higher-Order Model Checking," 
  CONCUR 2014,  pp.312-32, 2014

 * Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi:
   Automating relatively complete verification of higher-order functional programs,
   POPL 2013,  pp.75-86, 2013

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

 Applications to data compression: 
 * Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi,
   "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2012