[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://group-mmm.org/eratommsd/>) 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://group-mmm.org/eratommsd/open-position-for-a-postdoc-researcher-march... for full details. Thanks a lot for your consideration. Best, Ichiro ------------- JOB DESCRIPTION The candidate will work at National Institute of Informatics <https://www.nii.ac.jp/en/>, 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://group-mmm.org/~ichiro/> 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://doi.org/10.1007/978-3-030-25540-4_30> arXiv <https://arxiv.org/abs/1905.04486> (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://link.springer.com/chapter/10.1007/978-3-030-53291-8_19> arXiv <https://arxiv.org/abs/2007.07421> (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://doi.org/10.1007/978-3-030-25540-4_23> arXiv <https://arxiv.org/abs/1905.07549> (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://doi.org/10.1007/978-3-030-90870-6_17> (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://ieeexplore.ieee.org/document/9470656/> arXiv <https://arxiv.org/abs/2105.10164> (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://arxiv.org/abs/2203.14261> (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@acm.org Secretaries: hasuolab-secr@nii.ac.jp http://group-mmm.org/~ichiro/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]