From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10718 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Ichiro Hasuo Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.categories,gmane.science.mathematics.logic.coq.club Subject: Postdoc position in Tokyo: model checking and optimization metaheuristics Date: Tue, 19 Apr 2022 00:27:33 +0900 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============0694853095839383158==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="35084"; mail-complaints-to="usenet@ciao.gmane.io" To: types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, pvs-1VPwtPCARB1BDgjK7y7TUQ@public.gmane.org, hscc-bGTZWsvkwUHhn2KNwJGQxje48wsgrGvP@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Tue Apr 19 11:10:16 2022 Return-path: Envelope-to: gcst-types-announce@m.gmane-mx.org Original-Received: from mx0a-00390e01.pphosted.com ([148.163.133.158]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1ngjsG-0008yc-3u for gcst-types-announce@m.gmane-mx.org; Tue, 19 Apr 2022 11:10:16 +0200 Original-Received: from pps.filterd (m0172791.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with ESMTP id 23IMg8Sr012036; Tue, 19 Apr 2022 05:09:23 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com (PPS) with ESMTP id 3fgb05j55v-1; Tue, 19 Apr 2022 05:09:22 -0400 Original-Received: from RHIZOME.seas.upenn.edu (RHIZOME.SEAS.UPENN.EDU [158.130.69.24]) by leopard.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 23J99Fqn129673; Tue, 19 Apr 2022 05:09:15 -0400 Original-Received: from rhizome.seas.upenn.edu (localhost.upenn.edu [127.0.0.1]) by RHIZOME.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 23J99Ffb099478; Tue, 19 Apr 2022 05:09:15 -0400 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from mx0b-00390e01.pphosted.com (mx0b-00390e01.pphosted.com [148.163.137.158]) by RHIZOME.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 23IFRkil110852 for ; Mon, 18 Apr 2022 11:27:46 -0400 Original-Received: from pps.filterd (m0172793.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with ESMTP id 23IF9Xgv030216 for ; Mon, 18 Apr 2022 11:27:46 -0400 Original-Received: from mail-ej1-f43.google.com (mail-ej1-f43.google.com [209.85.218.43]) by mx0b-00390e01.pphosted.com (PPS) with ESMTPS id 3fgbaxpuh2-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Mon, 18 Apr 2022 11:27:46 -0400 Original-Received: by mail-ej1-f43.google.com with SMTP id ck12so5921463ejb.4 for ; Mon, 18 Apr 2022 08:27:45 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=jIsQgiq2D8rZZFJD0ZS84wz5gylK5Q6Toe3lnEEMMWQ=; b=7WicGek/BIUJxg3I9UTJm++f0N3jjq+vz/883KuNG6KHI/lvhFsR/wkJHRJb5DcSG2 fTestF+Pntsu4EI6HaKw8qhWvLgbudZ9Ur4CXzZJQvf1fANExaY41gze9zAY4o+NKiBn jlD2XrFNSuPrfomJJ/rXAyBGagRBroXGWfZpHDxPZO8mw5ka/RwlnAyy48XbRVJdMElA 4FAQ+SZ1hQDHyUgve4fhfTOtQ43DMEfuQMUU+ZmyMFM2dyScmhc3kpFrnZnEr4M7iNPl +goWsoH8Ns5gpBFLGTgtnurylsLYpX0Y4P26IOOidWjiyW1qRuuY65QJV3uRJuw9sc+3 zusw== X-Gm-Message-State: AOAM533obbwgEQY0XwRaSXmqj6UTKIjc2G2qk/g1ksNO7AChUNWcIpst 7guS5TfQA7NrKuEh0wxIwwTjyPRXBou31fTWb1fzUFYxuXsXyw== X-Google-Smtp-Source: ABdhPJyjLzMMOxm1vKvvlzbvv06Wl/5pI53hxCF3cBXoHbqXZhG+ePtbpP9ZhADNqDtPcetFfcTbzIRN8oS5OegzxPo= X-Received: by 2002:a17:907:72d5:b0:6ef:a49f:133a with SMTP id du21-20020a17090772d500b006efa49f133amr5293983ejc.420.1650295664166; Mon, 18 Apr 2022 08:27:44 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.858,Hydra:6.0.486,FMLib:17.11.64.514 definitions=2022-04-18_02,2022-04-15_01,2022-02-23_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 mlxlogscore=857 phishscore=0 adultscore=0 priorityscore=0 clxscore=238 bulkscore=0 lowpriorityscore=0 malwarescore=0 spamscore=0 impostorscore=0 mlxscore=0 suspectscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2202240000 definitions=main-2204180091 domainage_hfrom=11021 X-Mailman-Approved-At: Tue, 19 Apr 2022 05:09:11 -0400 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.35 Precedence: list List-Id: Announcements of interest to the TYPES community List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Original-Sender: "Types-announce" X-Proofpoint-GUID: xV2L8hOYpwBkAFNZJlBQJ0S7xL5XP4CQ X-Proofpoint-ORIG-GUID: xV2L8hOYpwBkAFNZJlBQJ0S7xL5XP4CQ X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.858,Hydra:6.0.486,FMLib:17.11.64.514 definitions=2022-04-19_03,2022-04-15_01,2022-02-23_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 malwarescore=0 suspectscore=0 bulkscore=0 clxscore=1011 priorityscore=1501 spamscore=0 adultscore=0 impostorscore=0 mlxscore=0 phishscore=0 lowpriorityscore=0 mlxlogscore=999 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2202240000 definitions=main-2204190051 Xref: news.gmane.io gmane.comp.science.types.announce:10256 gmane.science.mathematics.categories:10718 gmane.science.mathematics.logic.coq.club:23129 Archived-At: --===============0694853095839383158== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --===============0694853095839383158== Content-Type: multipart/alternative; boundary="000000000000d6494805dcef6650" --000000000000d6494805dcef6650 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable [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 ) 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-f= or-a-postdoc-researcher-march-2022/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJ= jFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntWM2LN3g$=20 for full details. Thanks a lot for your consideration. Best, Ichiro ------------- JOB DESCRIPTION The candidate will work at National Institute of Informatics , = 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 *lightwe= ight 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 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, =C3=89tienne Andr=C3=A9, Ichiro Hasuo: Symbolic Monitorin= g Against Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi arXiv (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 arXiv (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-42= 0. doi arXiv (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 (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 arXiv (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 (Another categorical work, but with a big emphasis on implementation. You are expected to be familiar with or eager for both.) =3D=3D=3D=3D=3D=3D Ichiro Hasuo Professor, National Institute of Informatics i.hasuo-HInyCGIudOg@public.gmane.org Secretaries: hasuolab-secr-5aC7G4kDdWR4Eiagz67IpQ@public.gmane.org https://urldefense.com/v3/__http://group-mmm.org/*ichiro/__;fg!!IBzWLUs!BDZ= N4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZnuSRsi59A= $=20 --000000000000d6494805dcef6650 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable
[Please distribute, apologies for multiple postings.]
=
Open Position for a PostDoc Researcher=C2=A0
(Mode= l Checking Extended with Optimization Metaheuristics, April 2022)

ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD) 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 problem= s that are complex and black-box. We aim to do so, at the same time, in a w= ay 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 suite= d for those who have experience in model checking research and who wish to = expand their research portfolio.=C2=A0

Some fu= rther details are found below. See
Best, Ichiro

<= /div>

-------------

JOB DESCRIPTION

The candidate will work at National Institute of Informatics= , Tokyo, Japan, and will pursue a novel extension of model checking techniq= ues (temporal logic, automata theory) with optimization metaheuristics (evo= lutionary computation, stochastic optimization, statistical machine learnin= g).

The goal is to overcome two major challenges that currently limit the ap= plicability of formal verification techniques to real-world industrial syst= ems, namely scalability and the absence of white-box models. In our endeavor towards the goal, we do not mind relying on testing, ra= ther than exhaustive verification; this puts us somewhat closer to so-calle= d lightweight formal methods.

That said, our theoretical development shall be nothing "lightweigh= t." We believe that there is a great theoretical depth here--we will e= xplore the depth using logical, automata-theoretic, and/or categorical mach= inery. This theory of "lightweight" formal methods<= /em> will significantly expand the current landscape of application of logi= c 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 in= dustrial collaborations and seek applicability to those real-world problems= (they are mostly from the manufacturing industry). At the same time, we se= ek rigorous logical/automata-theoretic/categorical foundations for the solu= tions we come up with--so our work stays well in the realm of the formal ve= rification community. We work in an interdisciplinary environment, and the = candidate will be constantly exposed to interaction with control theory, so= ftware engineering, automated driving, and category theory.

The candidate will work closely with Prof. Ichiro Hasuo and a few other team members. It is possible that the candidate be grant= ed an academic title (such as Project Assistant/Associate Professor).

References

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

  • Masaki Waga, =C3=89tienne Andr=C3=A9, Ichiro Hasuo: Symbolic Monito= ring Against Specifications Parametric in Time and Data. CAV (1) 2019: 520-= 539. doi arXiv
    (The to= pic is the theory of timed automata, which strikes a balance between theory= and applicability.)
  • Kittiphon Phalakarn, Toru Takisaka, Thomas H= aas, Ichiro Hasuo: Widest Paths and Global Propagation in Bounded Value Ite= ration for Stochastic Games. CAV (2) 2020: 349-371 doi arXiv
    (A work on a rathe= r classic topic in formal verification, but the algorithm is approximate an= d highly scalable. The basic idea behind the algorithm has potential extens= ions, both theoretically and practically)
  • Zhenya Zhang, Ichiro Hasu= o, Paolo Arcaini: Multi-armed Bandits for Boolean Connectives in Hybrid Sys= tem Falsification. CAV (1) 2019: 401-420. doi arXiv
    (The work exploits logical structures to orga= nize optimization metaheuristics on continuous domains.)
  • Sota Sato,= Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo: Hybrid System Fa= lsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case= Study. FM 2021: 313-329. doi
    (A real-wor= ld case study of logically structured optimization metaheuristics)
  • = Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, Ichiro Has= uo: Expressivity of Quantitative Modal Logics : Categorical Foundations via= Codensity and Approximation. LICS 2021: 1-14. = doi arXiv
    (A categorical work, a potential founda= tion of our theory. If this paper is your closest match, please note that y= ou are expected to be eager in working with optimization metaheuristics too= .)
  • Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ic= hiro Hasuo: The Lattice-Theoretic Essence of Property Directed Reachability= Analysis. CoRR abs/2203.14261 (2022) arXiv
    (Another = categorical work, but with a big emphasis on implementation. You are expect= ed to be familiar with or eager for both.)
=3D=3D=3D=3D=3D=3D
Ichiro Hasuo
Professor, National Institute of In= formatics
i.hasuo@a= cm.org =C2=A0 =C2=A0 Secretaries: hasuolab-secr-5aC7G4kDdWR4Eiagz67IpQ@public.gmane.org
http://group-mmm.org/~ichiro/
--000000000000d6494805dcef6650-- --===============0694853095839383158==--