2022年11月25-27日，2022年CCF中国软件大会（CCF ChinaSoft 2022）将于线上举行。大会将围绕“聚焦产教研用协同创新，提升关键软件供给能力”主题，举办包括学术、工业、教育等论坛活动40余场，预期有林惠民、陈左宁、邬江兴、何积丰、梅宏、吕建、柴洪峰、廖湘科、王怀民、郑纬民、蒋昌俊、王自力等10余位院士莅临，期待您的参与！

点击文末“阅读原文”即可报名注册线上参会！

https://conf.ccf.org.cn/chinasoft2022

✦  +

+

论坛巡礼

由华东师范大学、上海工业控制安全创新科技有限公司主办，科大国创软件股份有限公司、安徽中科国创高可信软件有限公司协办的【形式化方法工业应用前沿】技术分论坛将于11月27日上午举办。上海工业控制安全创新科技有限公司总经理 蒲戈光，国防科技大学计算机学院教授、博士生导师 董威共同担任本场论坛主席，来自科大国创、华东师大等知名企业高校的专家学者将于会上发表报告演讲，共话工业领域中形式化方法的落地实践。

论坛简介：

形式化方法利用数学推理与算法等作为主要技术，是保障软硬件可靠性与正确性的重要手段，如形式逻辑、程序证明与模型检测均为形式化方法领域的重要研究方向，过去有多位学者在这方向获得图灵奖。本论坛将介绍形式化方法在工业界的当前应用与实践情况，邀请了工业界与学术界的同行介绍形式化方法的应用实践以及遇到的挑战，覆盖了在芯片验证、操作系统验证、程序分析等应用领域。该论坛希望通过工业界与学术界的交流，共同讨论形式化方法在工业应用领域的优势与劣势，并从工业界发现有意义的学术问题，促进形式化方法领域学术共同体的发展。

日程安排

Schedule

      新品发布

高可信 · 高可用 · 高安全

✦  +

+

新品发布

随着软件产品对社会生产生活的重要性逐渐上升，如何改善并发展现有的软件工程方法，使其能对软件的安全可信提供更为可靠的保障，成为了工业界和学术界普遍关心的问题。传统软件工程中存在大量依赖人工的活动和主观性判断等过程和技术，给软件带来了明显的可信问题。形式化方法以其严谨的数学理论基础和不断发展的技术手段，被视为一种极有潜力的解决方案。鉴于此，中科国创高可信联合上海控安共同发布形式化软件工具链：“科创星云验证器（企业版）”& “SmartRocket Modeler可视化建模开发工具（beta版）”。这两款国产自研产品将形式化技术应用于实践，推动了形式化方法的深化与创新，为关键行业领域的数智化产品进一步提供了保障与支撑，也为中国乃至世界的软件安全保障提供了多种可能性。

（一）

公司：中科国创高可信

产品：科创星云验证器（企业版）

介绍：

科创星云验证器（企业版）采用自主设计的安全C规范语言作为规约语言，对程序的行为进行形式化描述。基于Hoare逻辑，采用最强后条件的演绎推理技术，将程序满足其形式规约的证明问题转化为一组数学命题的证明，并实现程序验证的自动化。科创星云验证器主要用于关键核心代码的验证，比如操作系统内核、数据库引擎、关键的嵌入式软件等，为航空航天、汽车电子、能源核电、轨道交通等安全攸关领域的高可信软件开发提供安全保障。

科创星云验证器（企业版）

官网：www.ustchcs.com

邮箱：info@ustchcs.com

电话：0551-65396781

（二）

公司：上海控安

产品：SmartRocket Modeler可视化建模开发工具

介绍：

SmartRocket Modeler是一款国产自主可控的可视化建模开发工具。该工具支持嵌入式软件模型的设计与开发，能够从系统需求出发，为用户提供基于Lustre模型语言的图形化建模、模型静态检查、模型仿真与调试、模型在环测试、C代码自动生成等丰富便捷的功能。同时工具也支持全系列国产操作系统，为国内高端制造领域的嵌入式软件研制提供支撑平台，为逐步摆脱对国外同类软件的依赖提供有效解决方案。

SmartRocket Modeler可视化建模开发工具（beta版）

官网：www.ticpsh.com

邮箱：Marketing@ticpsh.com

电话：021-62655886（工作日09:00-18:00）