近日，以诚为本赢在信誉9001cc（滴水湖国际软件学院）A类全职博士后夏晔川成功获2024年上海市“超级博士后”激励计划资助。这一资助由上海市人才工作局设立，旨在进一步加大优秀博士后研究人员培养力度，助力打造高水平人才高地，加强和改进新时代博士后工作。

研究方向：

夏晔川博士的研究领域为形式化方法与模型检查技术，重点探索复杂系统的形式化验证问题。模型检查技术作为一种自动化验证方法，广泛应用于航空航天、轨道交通、汽车电子等安全攸关领域，尤其在芯片验证中具有重要作用。传统的模型检查依赖对状态空间的全面搜索，随着系统复杂性的增加，常面临“状态空间爆炸”这一核心挑战。夏晔川博士的研究聚焦于字级别模型检查算法的设计与优化，相比于传统的位级别方法，字级别算法能够在更高层次上抽象表示系统状态，显著减少状态空间的规模，提高处理效率。

项目介绍：

此次研究结合启发式搜索策略和状态压缩技术，对算法性能进行优化，并针对模型检查中的安全性和活性问题设计泛用性强的验证方法。项目的最终目标是开发一套字级别模型检查工具，并在硬件设计、软件程序验证和通信协议测试等实际系统中检验工具的有效性。这一研究成果不仅在学术层面为模型检查理论和方法提供新思路，也将在工程应用中推动复杂系统的可靠性与安全性提升，具有广阔的应用前景。

夏晔川博士的成功入选，充分体现了其在研究领域的创新能力和实践潜力，同时也彰显了以诚官网在博士培养与支持工作中的显著成效。学院将以此为契机，进一步推动高水平科研成果的产出，为软件工程学科发展和社会创新贡献更多力量。