Staff図 2 本研究室が提案した新しい理論フレ ー ムワー クFig.2 The new theoretical framework proposed by our laboratory Clovis EberhartAssistant ProfessorIn 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)図 1 本研究室で研究開発中のプログラム検証・合成ツ ー ル群 CoARFig.1 The CoAR suite of program verification and synthesis tools developed and maintained in our laboratory海野 広志教授Hiroshi UnnoProfessor現代社会において、人々は日常的にスマートフォンやコンピュータを私生活や仕事に用いており、普段意識されない交通・金融・医療・エネルギーといった社会基盤もコンピュータにより制御されている。したがって、コンピュータを動かすプログラムであるソフトウェアの信頼性を確保し、効率性を向上させることは、社会の安定と円滑な機能の維持にとって重要な課題となっている。本研究室では、形式論理やプログラム理論といった基礎理論に基づいた高信頼・高効率ソフトウェア構成技術の研究を行っている。本分野では、与えられたプログラムがその仕様を満たすことを数学的に厳密に保証するための技術であるプログラム検証や、仕様からそれを満たすプログラムを生成するための技術であるプログラム合成の研究・開発を進めている。具体的には、関数型プログラミング言語 OCaml に検証・合成ツールを統合することによって、高信頼・高効率プログラムの開発を促進することを目指した RCaml や、多様な検証・合成問題を述語制約や不動点論理式として表現して解くことができるソルバである PCSat や MuVal, MuCyc の研究・開発を行っている。また、これらのツールの基礎となるプログラム理論や型理論、制約解消・最適化の理論、不動点論理とその演繹体系についても研究を行っている。特に最近のソフトウェアは、並行・並列・分散的な動作や機械学習モデルへの依存、暗号プロトコルや確率プログラム、乱択アルゴリズムにおけるランダム性の本質的な利用などにより、ますます複雑化している。そのため、既存の理論だけでは対処しきれない複雑性に対処するための理論構築にも力を注いでいる。Clovis Eberhart助教研究活動ソフトウェア構成研究分野｜海野教授34電気通信研究所 RIEC 2025／2026情報通信基盤研究部門Information Communication Platforms Division計算システム基盤研究部門Computing System Platforms Division人間・生体情報システム研究部門Human and Bio Information Systems Divisionナノ・スピン実験施設Laboratory for Nanoelectronics and Spintronicsブレインウェア研究開発施設Laboratory for Brainware Systemsソフトウェア構成研究室Software Construction
元のページ ../index.html#36