Researcher

Personal page

https://www.riec.tohoku.ac.jp/~unno/

Research Activities

In modern society, people regularly use smartphones and computers in their personal lives and work, and unnoticed, computer-controlled infrastructure such as transportation, finance, healthcare, and energy plays a crucial role. Therefore, ensuring the reliability of software that controls computers and improving its efficiency are important challenges for maintaining social stability and smooth functioning. In our laboratory, we research techniques to construct highly reliable and efficient software, based on foundational theories like formal logic and program theory.

Software Construction (Prof. Unno)

Research topics

• Program verification and program synthesis
• Programming languages and type systems
• Constraint solving and optimization
• Automated theorem proving

Our research focuses on program verification, which is a technique to mathematically rigorously guarantee that a given program satisfies its specification, and on program synthesis, which is a technique to generate programs that meet a given specification. Specifically, we are working on integrating verification and synthesis tools into the functional programming language OCaml, aiming to promote the development of highly reliable and efficient programs. Additionally, we are conducting research and development on solvers such as PCSat, MuVal, and MuCyc, which can represent and solve a variety of verification and synthesis problems as predicate constraints or fixed-point logical formulas.
Furthermore, we are conducting research on the theoretical foundations of these tools, including program theory, type theory, constraint solving, optimization theory, fixed-point logic, and its deductive systems. Especially, with the increasing complexity of recent software due to factors such as concurrent, parallel, and distributed behavior, reliance on machine learning models, and the inherent utilization of randomness in cryptographic protocols, probabilistic programs, and randomized algorithms, we are directing efforts towards constructing theories to address complexities beyond those covered by existing theories.