[TYPES/announce] Postdoc position in Tokyo: model checking and optimization metaheuristics

Mon Apr 18 11:27:33 EDT 2022

[Please distribute, apologies for multiple postings.]

Open Position for a PostDoc Researcher
(Model Checking Extended with Optimization Metaheuristics, April 2022)

ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD
<https://urldefense.com/v3/__https://group-mmm.org/eratommsd/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvmkdVIGw$ >) invites applications for a postdoc
researcher. We aim to combine model checking and optimization
metaheuristics, in order to scale formal verification techniques up to
real-world industrial problems that are complex and black-box. We aim to do
so, at the same time, in a way guided by solid meta-theoretical foundations
such as those which we've presented in LICS and CAV. We thus explore new
shapes of application of logic to modern software and systems. The position
will be especially suited for those who have experience in model checking
research and who wish to expand their research portfolio.

Some further details are found below. See
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/open-position-for-a-postdoc-researcher-march-2022/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntWM2LN3g$ 
for full details.

Thanks a lot for your consideration.
Best, Ichiro

-------------
JOB DESCRIPTION

The candidate will work at National Institute of Informatics
<https://urldefense.com/v3/__https://www.nii.ac.jp/en/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnuG1qA_zw$ >, Tokyo, Japan, and will pursue a novel
extension of model checking techniques (temporal logic, automata theory)
with optimization metaheuristics (evolutionary computation, stochastic
optimization, statistical machine learning).

The goal is to overcome two major challenges that currently limit the
applicability of formal verification techniques to real-world industrial
systems, namely *scalability* and the *absence of white-box models*. In our
endeavor towards the goal, we do not mind relying on testing, rather than
exhaustive verification; this puts us somewhat closer to so-called *lightweight
formal methods*.

That said, our theoretical development shall be nothing "lightweight." We
believe that there is a great theoretical depth here--we will explore the
depth using logical, automata-theoretic, and/or categorical machinery.
This *theory
of * *"lightweight" formal methods* will significantly expand the current
landscape of application of logic to software.

The position should be especially suited for model checking researchers who
wish to expand their research portfolio. We find case studies in our
industrial collaborations and seek applicability to those real-world
problems (they are mostly from the manufacturing industry). At the same
time, we seek rigorous logical/automata-theoretic/categorical foundations
for the solutions we come up with--so our work stays well in the realm of
the formal verification community. We work in an interdisciplinary
environment, and the candidate will be constantly exposed to interaction
with control theory, software engineering, automated driving, and category
theory.

The candidate will work closely with Prof. Ichiro Hasuo
<https://urldefense.com/v3/__https://group-mmm.org/*ichiro/__;fg!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvIjprMSA$ > and a few other team members. It is
possible that the candidate be granted an academic title (such as Project
Assistant/Associate Professor).
References

The following are some outcomes of our efforts so far. They are listed here
in order to exemplify concrete topics. Note that the topics of these papers
are diverse, and the candidate is not expected to follow all of them. A
good match with one of them would suffice.

   - Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring Against
   Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi
   <https://urldefense.com/v3/__https://doi.org/10.1007/978-3-030-25540-4_30__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvga5DGng$ > arXiv
   <https://urldefense.com/v3/__https://arxiv.org/abs/1905.04486__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnu9kaTOGw$ >
   (The topic is the theory of timed automata, which strikes a balance
   between theory and applicability.)
   - Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo: Widest
   Paths and Global Propagation in Bounded Value Iteration for Stochastic
   Games. CAV (2) 2020: 349-371 doi
   <https://urldefense.com/v3/__https://link.springer.com/chapter/10.1007/978-3-030-53291-8_19__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnsMk8ASZA$ > arXiv
   <https://urldefense.com/v3/__https://arxiv.org/abs/2007.07421__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntOut_yGA$ >
   (A work on a rather classic topic in formal verification, but the
   algorithm is approximate and highly scalable. The basic idea behind the
   algorithm has potential extensions, both theoretically and practically)
   - Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini: Multi-armed Bandits for
   Boolean Connectives in Hybrid System Falsification. CAV (1) 2019: 401-420.
   doi <https://urldefense.com/v3/__https://doi.org/10.1007/978-3-030-25540-4_23__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntRMSa89A$ > arXiv
   <https://urldefense.com/v3/__https://arxiv.org/abs/1905.07549__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvbf4uKDQ$ >
   (The work exploits logical structures to organize optimization
   metaheuristics on continuous domains.)
   - Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo:
   Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A
   Gas Turbine Case Study. FM 2021: 313-329. doi
   <https://urldefense.com/v3/__https://doi.org/10.1007/978-3-030-90870-6_17__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZns7LBdTWw$ >
   (A real-world case study of logically structured optimization
   metaheuristics)
   - Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot,
   Ichiro Hasuo: Expressivity of Quantitative Modal Logics : Categorical
   Foundations via Codensity and Approximation. LICS 2021: 1-14. doi
   <https://urldefense.com/v3/__https://ieeexplore.ieee.org/document/9470656/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvwujtkzA$ > arXiv
   <https://urldefense.com/v3/__https://arxiv.org/abs/2105.10164__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnt-4pYrzw$ >
   (A categorical work, a potential foundation of our theory. If this paper
   is your closest match, please note that you are expected to be eager in
   working with optimization metaheuristics too.)
   - Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro
   Hasuo: The Lattice-Theoretic Essence of Property Directed Reachability
   Analysis. CoRR abs/2203.14261 (2022) arXiv
   <https://urldefense.com/v3/__https://arxiv.org/abs/2203.14261__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnvzG1ylqQ$ >
   (Another categorical work, but with a big emphasis on implementation.
   You are expected to be familiar with or eager for both.)

======
Ichiro Hasuo
Professor, National Institute of Informatics
i.hasuo at acm.org     Secretaries: hasuolab-secr at nii.ac.jp
https://urldefense.com/v3/__http://group-mmm.org/*ichiro/__;fg!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnuSRsi59A$ 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220419/498edf8a/attachment-0001.htm>