Chitose International Forum
on Science & Technology 2026

Beyond Coding: Empowering the Next Generation through Community-Supported Programming Education

Assoc. Prof. Hiroto Yamakawa

Chitose Institute of Science and Technology

Programming is becoming an important part of school education in many countries. Although students learn the basics of programming in school, they do not always have enough opportunities to use these skills to solve problems in their daily lives. Local communities can help fill this gap by providing practical learning experiences outside the classroom.
This tutorial introduces our community-based approach to programming education through activities in Chitose City and the Hokkaido Java User Group. In these activities, university students, software engineers, teachers, and local volunteers work together to support children’s learning. Rather than simply teaching programming, we encourage children to find problems around them, think about possible solutions, and use programming as a tool to solve them.
Participants will first learn about programming education in Japanese schools and the role of local communities in supporting children’s learning. After experiencing a simple programming activity, they will work in small groups to design a programming lesson for elementary school students based on everyday problems.
Through these activities, participants will explore how university students, software engineers, and local communities can work together to create meaningful learning opportunities for the next generation.

Formalization and Verification of Security Properties in Security Protocols

Prof. Shigeki Hagihara

Chitose Institute of Science and Technology

Security protocols are widely used to achieve various security goals, such as confidentiality, authentication, and anonymity. However, determining whether a protocol actually satisfies its intended security properties requires these properties to be precisely specified and rigorously verified. This tutorial provides an introduction to the formalization and verification of security properties in security protocols.
We first discuss typical security properties expected of security protocols and examine how informal security requirements can be expressed precisely using formal models. We then introduce fundamental approaches to the formal verification of these properties, focusing on how security guarantees can be specified and analyzed systematically. The tutorial covers representative verification techniques and explains the principles behind their application to security protocols.
The tutorial also highlights the relationship between the security properties being verified and the underlying models used for verification, helping participants understand the assumptions and abstractions involved in formal security analysis. Finally, we briefly introduce research on the relationship between symbolic and computational models, and discuss how results obtained in symbolic models can be related to security guarantees in computational models.
The tutorial is intended to provide participants with a systematic understanding of how security properties are formalized and verified, and to serve as an entry point to formal methods for rigorous security analysis.