形式化方法与应用专题前言

形式化方法是采用数学方法,对复杂计算机系统建立严格语法与语义规范的系统设计与验证方法,常用于复杂动态系统的需求规约、模型设计和属性验证,在计算机硬件设计、软件系统构造、控制系统模型设计与分析、通信系统协议验证和程序代码合成等方面得到了成功的应用.近年来,在深度学习、区块链、量子计算、物理信息融合系统等新兴领域,形式化方法也逐步应用和适配,对提升系统的安全性和可靠性起到了极大的促进作用.     

形式化方法与应用专题前言

计算机科学的发展主要涉及硬件和软件的发展,而软、硬件发展的核心问题之一是如何保证它们是安全可靠的.如今,硬件性能变得越来越高,运算速度也越来越快,体系结构、软件的功能也更加复杂,如何开发可靠的软、硬件系统,是计算机科学发展面临的巨大挑战.特别是现在计算机系统广泛应用于许多安全攸关系统中,如高速列车控制系统、航空航天控制...     

软件形式化方法与应用专题前言

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专刊收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.     

面向新兴系统的形式化建模与验证方法专题前言

<正>形式化方法是计算机科学的重要理论基础.它以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法.近年来,随着相关技术的发展,形式化方法已经在越来越多的新兴系统中得到应用并取得显著效果.为了记录中国学者在新兴系统的形式化建模与验证理论、方法、工具和应用等方面的最新研究成果,特设立此专题.本专题采取自由投稿的方式,共收到17篇投稿,其中16篇通过了形式审查.特邀编辑邀请17位领域专家参     

形式化方法与工具专刊前言

形式化方法是指有严格数学基础的软件和系统开发方法,支持计算机系统及软件的规约、设计、验证与演化等活动.随着高可信软件的兴起,形式化方法作为重要的途径,关注度日益提高.其作用不仅深化了人们对计算系统规律的认识,而且支持了计算系统开发、运行和演化之工具、平台、环境的构建.本专刊收录的11篇论文反映了近年来我国学者在形式化方法与工具领域的部分研究成果.     

定理证明理论与应用专题前言

<正>随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.近年来,定理证明已经逐步用于越来越多的软件、硬件系统验证,这一方面为软硬件系统的安全性保障提供了新的有力工具,另一方面也成为定理证明技术发展的有利契机.目前,定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要,对于数学分析、离散数学、概率等基础定理证明库或求解方案的需求也越来越迫切.     

优青专题前言

优秀青年科学基金(“优青基金”)是国家自然科学基金委员会2012年起设立的一类人才项目,主要支持在基础研究方面已取得较好成绩的青年学者自主选择研究方向开展创新研究,至今已经资助了5期。为了集中介绍这些优秀青年学者的研究成果,本刊推出了“优青专题”系列,并已于2015年和2016年出版了两个专辑,本期是该系列的第三个专辑,共13篇文章。与前两次专辑一样,本专辑并不专注于介绍计算机科学技术领域某个特定方向的研究和发展状况,而是为优青基金获得者提供展示他们（及其合作者）研究成果、传播相关知识的综合平台,同时可以使得有关读者通过该专辑了解我国这一层次研究人员的研究状况及相关领域发展的趋势。我们希望本系列专辑的出版能为作者、读者提供一个开放的交流平台,促进计算机科学技术领域的研究、开发、教育和前沿知识的传播。