Yoriyuki Yamagata
Faculty of Engineering, University of Fukui
Research Interests
My work centers on mathematical logic and its applications. It spans formal methods, software verification, and the reliability of cyber-physical systems, as well as bounded arithmetic and computational complexity in mathematical logic—addressing software reliability from both theoretical and practical perspectives. Recently I am especially interested in applying AI to software verification. My current research falls into the four areas below.
1. Assurance for the Software Supply Chain
Building and deploying software today means relying on a large number of existing packages, development environments, and deployment environments. As a result, developers themselves often cannot fully assess properties like security. I approach this problem using assurance cases — structured documents, borrowed from safety engineering, that explain why a system can be trusted in terms domain experts can follow. In particular, I have developed PGSN, a programming language specialized for manipulating GSN (Goal Structured Notation), the diagrammatic notation commonly used to write assurance cases. PGSN is a purely functional language, which gives it useful properties: results do not depend on evaluation order, and the type system guarantees the validity of its output.
2. Formal Verification of Cyber-Physical Systems
Public infrastructure such as water systems, power grids, and railways is controlled by computers. A system that integrates the information space created by computers (cyberspace) with a physical system such as a power grid (physical space) is called a cyber-physical system (CPS). The reliability of CPS is an important social concern, but their complexity makes it hard to guarantee. I work on this problem mainly through formal methods.
Counterexample generation: Fully verifying a CPS formally is generally infeasible, so instead the correct behavior of a system is specified in temporal logic, and various optimization techniques are used to search for inputs that drive the system into incorrect behavior. I have developed a method for this search based on deep reinforcement learning.
Temporal logic for stochastic processes: Because CPS behavior is uncertain, it is naturally modeled as a stochastic process — yet the theoretical foundations for applying temporal logic to stochastic processes are not fully worked out. I have studied this mathematically, establishing results such as the measurability of the event that a temporal-logic formula is satisfied (a prerequisite for applying probability theory), the fact that a continuous-time interpretation is not always the limit of discrete-time interpretations, and conditions under which it is.
Statistical anomaly detection: Separately from formal methods, I also work on detecting anomalies in CPS using purely machine-learning-based techniques.
3. Bounded Arithmetic and Computational Complexity
Questions about computational complexity — such as whether P equals NP — are among the most fundamental open problems in the field. Bounded arithmetic is a family of logical systems for reasoning about natural numbers in which mathematical induction is restricted to apply only to statements only quantifying over finite number of integers. It is known that separating the various classes of bounded arithmetic is closely tied to separating complexity classes, so I approach open problems in computational complexity from the perspective of bounded arithmetic.
4. COVID-19 Epidemic Simulation
Outside my main area of expertise, I have drawn on my experience building machine-learning software to work on predicting COVID-19 infections from mobile location data. The simulator itself is not machine-learning-based — it is grounded in epidemiology — but it uses PyTorch to run large-scale models efficiently on GPUs.
Career
- Jan 2025 – presentAssociate Professor, Graduate School of Engineering, University of Fukui
- Nov 2018 – Dec 2024Senior Researcher, Cyber Physical Security Research Center, AIST
- Apr 2015 – Oct 2018Senior Researcher, Information Technology Research Institute, AIST
- Mar 2013 – Mar 2015Senior Researcher, Research Institute for Secure Systems, AIST
- Apr 2012 – Feb 2013Researcher, Research Institute for Secure Systems, AIST
- Apr 2010 – Mar 2012Researcher, Research Center for Embedded Systems, AIST
- Apr 2008 – Mar 2010Researcher, Research Center for Verification and Semantics, AIST
- Apr 2005 – Mar 2008Fixed-term Researcher, Research Center for Verification and Semantics, AIST
- Aug 2004 – Mar 2005Special Researcher, Research Center for Verification and Semantics, AIST
- Sep 2002 – Mar 2003Part-time Lecturer, Department of Mathematics, Tokyo Metropolitan University
Education
- Apr 1997 – Mar 2002PhD, Graduate School of Mathematical Sciences, University of Tokyo
- Apr 1995 – Mar 1997Department of Mathematics, Faculty of Science, University of Tokyo
- Apr 1993 – Mar 1995College of Arts and Sciences (Science I), University of Tokyo
Skills
Programming Languages
OS & Frameworks
Languages
Hobbies
Outside of research, I enjoy playing the piano — not only classical repertoire, but also film and anime scores such as the soundtrack of Violet Evergarden. (Though I should warn you: pieces I'm not actively practicing fade fast, so please don't ask me to perform on the spot!) I also enjoy reading, especially philosophy, history, nonfiction, and manga.