[TYPES/announce] Open Postdoc Position on Higher-Order Model Checking
koba at kb.is.s.u-tokyo.ac.jp
koba at kb.is.s.u-tokyo.ac.jp
Mon Nov 28 20:45:54 EST 2016
A postdoc position is available for a project on Higher-Order Model
Checking (see the project description below), at the University of
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
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.
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
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
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,"
[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,"
[UTK13] Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi:
Automating relatively complete verification of higher-order functional programs,
[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
More information about the Types-announce