抽象解释及其应用研究进展

抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.

基于指向与数值抽象的带指针算术程序的分析方法

带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。

基于抽象解释的函数内联过程间分析优化方法

分析实际程序时往往需要分析程序中函数的调用,一般使用过程间分析来实现全程序分析.函数内联是一种最为精确、易于实现的过程间分析方法.通过函数内联,可以使得已有过程内分析方法和工具支持包含函数调用的程序的分析.但是函数内联后代码的规模急剧增加,同时将产生大量中间变量,增加程序分析的变量维度,导致程序分析过程时空开销大大增加.考虑基于抽象解释框架下函数内联过程间分析的一些不足,并提出了相应的优化方法.基于抽象解释的程序分析关注自动推导程序变量之间的不变式约束关系,因此程序变量构成的程序环境大小(即各程序点处须考虑的相关变量集合)对分析的时空开销具有重要影响.为了减少函数内联后程序分析的开销,提出了面向内联函数块的程序环境降维优化方法.该方法针对内联函数后的程序代码,分析确定不同程序点处需维护的程序环境(即相关变量集合),而不是所有程序点共享同一全局程序环境,从而实现程序状态的降维.详细描述了基于该方法所实现的工具DRIP(dimension reduction for analyzing function inlined program)的架构、模块及算法细节.并在WCET Benchmarks测试集开展了分析实验.实验结果表明:DRIP在变量消除上取得的效果良好,甚至在某些测试集上能减少一半以上的变量,并在一定程度上降低了分析过程的时空开销.

群体化学习及其在计算机课程中的应用

针对知识快速更新背景下教学活动资源建设与问题解决的问题,借鉴群体化开发社区与问答社区的协作机理,提出群体化学习模型,介绍开发的支撑平台"知士荟"在两个计算机类课程中的应用情况,基于学生的反馈分析平台应用成效,指出将群体化学习应用在课堂教学中需要重点解决的若干问题。

基于区间线性模版约束的程序分析

抽象解释是一种对程序语义进行可靠近似的通用理论,该理论在保证可靠性的前提下,可为程序变量的值范围分析提供一个通用的框架.抽象域是抽象解释框架的核心,在该框架下面向数值性质分析的数值抽象域得到了广泛的关注.其中,模板多面体抽象域的表达能力覆盖了程序分析中常用的弱关系型抽象域,如区间抽象域、八边形抽象域等.该文对经典的基于线性模版约束的模版多面体抽象域进行扩展,以支持区间线性模版约束,从而得到一个新的数值抽象域——区间线性模版约束抽象域,可以用来推导变量间形如"∑k[a_k,b_k]x_k≤c"的区间线性不等式关系(其中区间系数[a_k,b_k]为分析前预先确定的常量).该抽象域采用"弱解"作为区间线性约束的解语义,可以表达某类非凸(甚至非联通)性质,因而比经典的模版多面体抽象域表达能力更强.区间线性模板约束抽象域的域元素可以看作是一系列模版多面体的析取,几何上,其域元素与每个象限的交均是一个凸的模板多面体(可以为空).该文给出了区间线性模版约束抽象域的域表示和域操作,基于该抽象域的静态分析算法主要基于区间线性规划来实现.进一步,该文讨论了基于区间线性模版约束抽象域中区间线性模版的生成方法.最后,该文在开源数值抽象库APRON中实现了区间线性模版约束抽象域,并开展了程序分析实验.初步的实验结果表明区间线性模版约束抽象域可以有效地分析程序中的析取行为.