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

[koba at kb.is.s.u-tokyo.ac.jp]

 A postdoc position is available for a 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 2017 (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 360,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 (ideally two or more) of
 the following topics: program verification, lambda-calculus and type
 systems, 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 January 20th, 2017.

 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 studied higher-order model checking (more precisely,
 HORS model checking, where the language for describing systems has been
 extended to higher-order), 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 [K13a], and that (ii) despite
 its extremely high worst-case complexity, higher-order model checking
 can be solved efficiently for many typical inputs [K13a,BK13]. 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 [KSU11,KSUK15,MTKSU16,WSTK16].
 Recently, we have also started investigating the other kind of higher-order model 
 checking called HFL model checking, where the logic used for describing properties
 has been extended to higher-order [KLB17].
 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 [KMSY12,TKYS16].

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

 * Theory and model checking algorithms:

 [KLB17] Naoki Kobayashi, Etienne Lozes, Florian Bruse,
    "On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic,"
    POPL 2017

 [K13a] Naoki Kobayashi, "Model Checking Higher-Order Programs," JACM, 2013.

 [K13b] Naoki Kobayashi, "Pumping by Typing," LICS 2013

 [BK13] Christopher H. Broadbent, Naoki Kobayashi,
   "Saturation-Based Model Checking of Higher-Order Recursion Schemes," CSL 2013

 * Applications to program verification:

 [WSTK16] Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi,
    "Automatically disproving fair termination of higher-order functional programs," ICFP 2016

 [MTKSU16] Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno,
    "Temporal verification of higher-order functional programs," POPL 2016

 [KSUK15] Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi,
  "Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs,"
   CAV 2015

 [UTK13] Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi:
   Automating relatively complete verification of higher-order functional programs,
   POPL 2013

 [KSU11] Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno,
  "Predicate Abstraction and CEGAR for Higher-Order Model Checking", PLDI 2011

 * Applications to data compression: 

 [TKYS16] Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara,
   "Compact bit encoding schemes for simply-typed lambda-terms," ICFP 2016

 [KMSY12] Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi,
   "Functional Programs as Compressed Data", Higher-Order and Symbolic Computation, 2012