海野 広志教授現代社会において、人々は日常的にスマートフォンやコンピュータを私生活や仕事に用いており、普段意識されない交通・金融・医療・エネルギーといった社会基盤もコンピュータにより制御されている。したがって、コンピュータを動かすプログラムであるソフトウェアの信頼性を確保し、効率性を向上させることは、社会の安定と円滑な機能の維持にとって重要な課題となっている。本研究室では、形式論理やプログラム理論といった基礎理論に基づいた高信頼・高効率ソフトウェア構成技術の研究を行っている。本分野では、与えられたプログラムがその仕様を満たすことを数学的に厳密に保証するための技術であるプログラム検証や、仕様からそれを満たすプログラムを生成するための技術であるプログラム合成の研究・開発を進めている。具体的には、関数型プログラミング言語 OCaml に検証・合成ツールを統合することによって、高信頼・高効率プログラムの開発を促進することを目指した RCaml や、多様な検証・合成問題を述語制約や不動点論理式として表現して解くことができるソルバである PCSat や MuVal, MuCyc の研究・開発を行っている。また、これらのツールの基礎となるプログラム理論や型理論、制約解消・最適化の理論、不動点論理とその演繹体系についても研究を行っている。特に最近のソフトウェアは、並行・並列・分散的な動作や機械学習モデルへの依存、暗号プロトコルや確率プログラム、乱択アルゴリズムにおけるランダム性の本質的な利用などにより、ますます複雑化している。そのため、既存の理論だけでは対処しきれない複雑性に対処するための理論構築にも力を注いでいる。図１ 開発した検証ツール MuVal の性能評価図２ 開発した自動定理証明ツール MuCyc による証明探索Fig.2 Proof Search with the Developed Automated Theorem Prover MuCycFig.1 Performance Evaluation of the Developed Verification Tool MuValHiroshi UnnoProfessor34In 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 for-mal logic and program theory.Our research focuses on program verification, which is a tech-nique 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 ver-ification 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 log-ic, and its deductive systems. Especially, with the increasing complexity of recent software due to factors such as concur-rent, parallel, and distributed behavior, reliance on machine learning models, and the inherent utilization of randomness in cryptographic protocols, probabilistic programs, and random-ized algorithms, we are directing efforts towards constructing theories to address complexities beyond those covered by existing theories.Research ActivitiesSoftware Construction (Prof. Unno)Staffソフトウェア構成研究室Software Construction研究活動ソフトウェア構成研究分野｜海野教授
元のページ ../index.html#36