A paper by Kittiphon Phalakarn, Ichiro Hasuo and other was awarded as the Best Paper Award of The 21st International Colloquium on Theoretical Aspects of Computing (ICTAC 2024).
Authors
Kittiphon Phalakarn（National Institute of Informatics ）
Sasinee Pruekprasert（National Institute of Advanced Industrial Science and Technology）
Ichiro Hasuo（National Institute of Informatics）
Awarded Paper Title
Winning Strategy Templates for Stochastic Parity Games Towards Permissive and Resilient Control
We invite applications for postdoc and senior researchers. The candidates will pursue collaboration with Bart Jacobs (Nijmegen), Joost-Pieter Katoen (Aachen), and Sam Staton (Oxford). The positions are for 4.5 years max.
Symposium information: https://group-mmm.org/eratommsd/ja/2024symposium/
Most talks are in Japanese… but join us for poster presentations and discussions! Registration deadline: Fri 7 June.
A paper by Mayuko Kori, Ichiro Hasuo and others was awarded as Distinguished Paper Award of 35th International Conference on Computer Aided Verification.
Authors
Mayuko Kori (National Institute of Informatics & SOKENDAI)
Flavio Ascari (University of Pisa)
Filippo Bonchi (University of Pisa)
Roberto Bruni (University of Pisa)
Roberta Gori (University of Pisa)
Ichiro Hasuo (National Institute of Informatics & SOKENDAI)
Awarded Paper Title
Exploiting Adjoints in Property Directed Reachability Analysis
Mayuko Kori is a PhD student at SOKENDAI/NII, a JSPS Research Fellow (DC), and a research assistant at ERATO MMSD (Group 0).
Three papers (co)-authored by ERATO MMSD researchers accepted for presentation at CAV 2023 – 35th International Conference on Computer Aided Verification.
The CAV Conference is a top international venue on computer-aided formal analysis methods for hardware and software systems. CAV 2023 will take place in Paris, Frande, in July 2023.
A few positions with us are now open:
Besides, there is a post-doc opportunity open in Kyoto, in Atsushi Igarashi’s group (we work closely with them):
A news release from NII and JST:
The research team led by HASUO Ichiro at the National Institute of Informatics (NII, Japan) developed a methodology to provide strong mathematical safety guarantees to automated driving vehicles, together with its underlying theory on formal logic. This research was conducted under the ERATO MMSD project funded by the Japan Science and Technology Agency (JST, Japan).
Building on the existing methodology called “Responsibility-Sensitive Safety (RSS)” for mathematical proofs of automated driving safety, the research established its extension called “Goal-Aware RSS (GA-RSS)” that expands RSS’s application domain to a variety of real-world driving scenarios. Specifically, the techniques in GA-RSS derived from theoretical results in formal logic enable one to provide mathematical safety proofs to more complex driving scenarios than before, especially those which require achievement of certain goals such as an emergency stop.
The outcome of this research was published in IEEE Transactions on Intelligent Vehicles, a top journal on automated driving on July 5, 2022 (US Eastern Time).
The following positions are currently open.
New method for automatic and efficient discovery of reliable gas turbine system designs
— Exploiting the logical specification in black box optimization and applying it to the design process of real commercial products — A research team consisting mainly of SATO Sota and HASUO Ichiro at the National Institute of Informatics (NII, Japan) and the Graduate University for Advanced Studies (SOKENDAI, Japan), developed a method for automatically finding gas turbine control system designs that satisfy multiple requirements, with collaboration of Mitsubishi Heavy Industries, Ltd.
Automatic control system design methods have not hitherto been able to discover controllers of comparable quality to those designed by human experts. But with the new method developed by this research team, it is now possible to find controllers with comparable quality to the results obtained manually by human experts, based on fully automatic computation. This method is generally applicable to “black box” control systems whose internal behavior cannot be described by models such as mathematical formulas. The method is expected to be useful in design processes in various fields such as autonomous driving.
This research was conducted under the ERATO MMSD Project（*1） funded by the Japan Science and Technology Agency (JST, Japan). The results of this research will be presented online on November 24, 2021 (Chinese Standard Time) at the 24th International Formal Methods Symposium (FM’21).
Dr. Paolo Arcaini has been awarded the Distinguished paper award at SSBSE 2021 — 13th Symposium on Search-Based Software Engineering
Xinyi Wang, Paolo Arcaini, Tao Yue, Shaukat Ali
Generating Failing Test Suites for Quantum Programs With Search
Dr. Paolo Arcaini is a Project Associate Professor at NII, and the leader of ERATO MMSD Project, Group 3.
