[TYPES/announce] Postdoc position on automated verification of higher-order programs
koba at kb.is.s.u-tokyo.ac.jp
Thu May 10 02:57:43 EDT 2012
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
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 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.
Naoki Kobayashi, "Types and Higher-Order Recursion Schemes for
Verification of Higher-Order Programs," Proceedings of POPL 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
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.
"Higher-Order Model Checking: From Theory to Practice",
Invited paper in Proceedings of LICS 2011.
(A very brief survery of the field)
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
More information about the Types-announce