We would like to offer internship opportunities to you. We prepare the following internship topics. The condition of the internship will be determined on a case-by-case basis. Let us know if you are interested in them.

1. Experiments on the verification of an automated driving system.
We are proposing formal methods to ensure the safety and reliability of automated system platforms. In the internship, you are supposed to join our project and conduct experiments on the verification of an automated driving system such as Autoware, in particular, about its perception module, planning module, and their system software.

2.Formal modeling and verification of automotive systems.
You will model a target system (in a scenario) using a language such as Simulink and Lustre, and then analyze the safety of the system using simulators, model checkers, etc. Example target systems: Autoware- vehicle, (controller node of) ROS-based robot, and vehicle system.

3.Development on a formal method tool (e.g. SMT solvers and automated theorem provers).
You will experiment with solving benchmark problem sets using an existing tool, and then try to improve the performance by modifying the encoding method, reasoning strategies, etc.