研究方向

基础软件与系统重点实验室（中国科学院）（以下简称实验室）2023年1月由中国科学院批准建设，依托单位为中国科学院软件研究所。

实验室在软件理论与基础软件方面具有深厚的研究积累，获我国信息技术领域首个国家自然科学一等奖，获软件理论国际顶会LICS与CAV我国首个杰出论文奖，研制我国第一个通过国标认证的安全操作系统，是RISC-V基础软件生态的国际核心贡献和引领者。实验室拥有我国多位计算机软件科学事业的奠基人和开拓者，实验室固定人员包括中国科学院院士3人、研究员（含正高级工程师）53人、副研究员（含高级工程师）38人等。

实验室的使命定位为我国基础软件的先锋队，即基础软件理论原始创新的引领者、基础软件关键核心技术的突破者、国际一流基础软件人才的集聚地，成为我国基础软件创新的国家战略科技力量之一。实验室自底向上从“理论-技术-系统”三个层次，设立“基础软件理论与形式化方法”、“基础软件高效开发与高可信保障技术”、“核心基础软件与系统”三个研究方向，开展贯通式研究，旨在实现我国基础软件的跨越式发展。

主要研究方向：

核心基础软件与系统　　聚焦操作系统等基础软件领域的“燃眉之急”和“心腹之患”问题，努力实现基础软件自主替代和开源软件可靠供应。重点研究面向开放指令集的基础软件核心技术，研制基于 RISC-V 的操作系统内核、编译工具链等，抢占 RISC-V技术生态高地；研究面向智能万物互联、新型人机交互的新一代操作系统；建设开源软件供应链基础设施平台，摆脱对国外“根社区”及操作系统等的开发与运行依赖。具体包括：基础软件核心组件，面向 RISC-V 的操作系统内核和开发运行环境，面向高性能计算机的基础数学库、基础算法库，约束求解器引擎，开源软件供应链基础设施平台，量子操作系统等。

软件原理与形式化方法　聚焦基础软件蕴含的科学问题，探索软件形式化方法、新型计算模型与程序设计等基础理论。重点研究计算模型、计算复杂性、算法、计算逻辑等；涵盖并发、实时、混成、移动、随机等行为特征的复杂系统的形式化方法，包括形式建模、形式语义、形式规约、形式验证等；复杂约束求解、组合优化及自动和半自动推理理论与技术；量子程序设计模型与程序逻辑。

基础软件高效开发与高可信保障技术　　聚焦“基础软件的高效开发与质量保障”技术问题，研究面向软件的高效开发和软件的正确性、可靠性、安全性技术难题，支撑复杂软件的建模、开发与质量保障。重点研究面向高可信保障的软件构造方法，基于群体智能的软件开发方法，软件分析测试与质量保障方法，软件安全保障与运行监控理论，软件供应链理论体系与构造方法，量子程序编译技术与系统，量子程序分析、测试、验证方法与工具。