单变量区间线性不等式抽象域

程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.     

基于抽象域和数值熵协同的数值程序分析

在软件日益丰富的信息时代,程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析,提取不变量的抽象域区间;在抽象域区间上进行数值熵运算;运行程序获取数值变量的实际取值,计算数值熵;将抽象域区间数值熵和实际数值熵信息进行对比分析,准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围,而引入数值熵算法,在取值范围的基础上对程序静态分析的准确性进一步检验,同时也做到了对程序的正确性验证。通过C语言程序实例,对抽象解释基础上的熵值分析方法进行了验证,证明了该分析方法的可行性和正确性。     

含有析取语义循环的不变式生成改进方法

抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.     

基于区间向量抽象域的数值程序分析算法

为权衡对矩阵运算静态分析的精度和效率,针对程序中表示矩阵的变量,提出一种基于抽象解释的抽象与分析算法,即区间向量抽象域。将矩阵变量抽象为一个区间向量对,即行区间向量和列区间向量,矩阵各元素的值范围是由这两个区间向量对应元素的交集表示;设计在该抽象域上的操作以及迁移函数。通过对区间向量抽象域的计算,较好地权衡矩阵元素值范围分析的精确度和分析效率。实验结果表明,该抽象域能够较精确地分析程序中矩阵各元素的值范围,与现有的分析数组的抽象域相比,在分析精度和效率之间取得了合理权衡。     

一个面向C和Fortran数值程序的静态分析工具

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。     

基于约束的多面体抽象域的弱接合

基于约束的多面体抽象域的处理能力主要受限于其高代价的(强)接合操作,即两多面体的凸闭包计算。针对基于约束的多面体抽象域提出了一系列低代价的弱接合操作,以作为凸闭包计算的可靠替代候选。为了能够在分析效率和精度之间取得合理权衡,还提出了一种启发式策略,以把强、弱接合动态地、有机地结合起来进行程序分析。实验结果表明,弱接合能够极大地提升基于约束的多面体抽象域的效率、可扩展性和鲁棒性。     

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

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

自动合成数组不变式

本文提出了一个基于抽象解释框架自动合成数组程序不变式的方法.它能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域,通过前向迭代数据流分析合成数组性质.本文证明了该方法的正确性和收敛性,并通过一些实例展示了该方法的灵活性.我们开发了一个原型工具.该工具在各种数组程序（包括Competition on Software Verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.     

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

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

充满魅力的计算机艺术图

利用计算机自动生成一些漂亮的艺术图形,这是十分有趣的,也充满魅力。在计算机自动生成艺术图形的方法中,有一种是利用函数迭代的方法来生成。其迭代公式为:x=a[k]*x+b[k]*y+e[k],y=c[k]*x+d[k]*y+f[k]。其中k取1、2、…、n,每一个k对应的一组参数a[k]、b[k]、c[k]、d[k]、e[k]、f[k]代表一种迭代法则,共有n种法则。在实际中,n可取4(本程序如此),并预先给定每组参数。在迭代     

分段延迟微分方程线性-方法数值解渐近稳定性

This paper deals with the stability analysis of numerical solutionof linear -methods for delay differential equations. We focuson the linear test equation x(t)=ax(t)+bx(［t］), where a,b areconstants and ［t］ is the largest-integer function. Sufficent conditionsare given for the numerical solution to be asymptotic stable     

A suite of abstract domains for static analysis of string values

Strings are widely used in modern programming languages in various scenarios. For instance, strings are used to build up Structured Query Language (SQL) queries that are then executed. Malformed strings may lead to subtle bugs, as well as non‐sanitized strings may raise security issues in an application. For these reasons, the application of static analysis to compute safety properties over string values at compile time is particularly appealing. In this article, we propose a generic approach for the static analysis of string values based on abstract interpretation. In particular, we design a suite of abstract semantics for strings, where each abstract domain tracks a different kind of information. We discuss the trade‐off between efficiency and accuracy when using such domains to catch the properties of interest. In this way, the analysis can be tuned at different levels of precision and efficiency, and it can address specific properties.Copyright © 2013 John Wiley & Sons, Ltd.     

The octagon abstract domain

This article presents the octagon abstract domain, a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form ± X ± Y ≤ c where X and Y range among program variables and c is a constant in ℤ, ℚ, or ℝ automatically inferred. Abstract elements are represented using modified Difference Bound Matrices and we use a normalization algorithm loosely based on the shortest-path closure to compute canonical representations and construct best-precision abstract transfer functions. We achieve a quadratic memory cost per abstract element and a cubic worst-case time cost per abstract operation, with respect to the number of program variables. In terms of cost and precision, our domain is in between the well-known fast but imprecise interval domain and the costly polyhedron domain. We show that it is precise enough to treat interesting examples requiring relational invariants, and hence, out of the reach of the interval domain. We also present a packing strategy that allows scaling our domain up to large programs by tuning the amount of relationality. The octagon domain was incorporated into the ASTRéE industrial-strength static analyzer and was key in proving the absence of run-time errors in large critical embedded flight control software for Airbus planes. This paper is the journal version of an earlier conference paper [44] sharing this title. However, the present version, extracted from the author’s PhD [46] is extended in many ways and enriched with new experimental results. Partially supported by the exploratory project ASTRéE of the Réseau National de recherche et d’innovation en Technologies Logicielles (RNTL).     

Verification of Real-Time Systems using Linear Relation Analysis

Linear Relation Analysis [11] is an abstract interpretation devoted to the automatic discovery of invariant linear inequalities among numerical variables of a program. In this paper, we apply such an analysis to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.     

Uniform Closures: Order-Theoretically Reconstructing Logic Program Semantics and Abstract Domain Refinements

The notion of uniform closure operator is introduced, and it is shown how this concept surfaces in two different areas of application of abstract interpretation, notably in semantics design for logic programs and in the theory of abstract domain refinements. In logic programming, uniform closures permit generalization, from an order-theoretic perspective, of the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the model-theoretic characterization of the well-known s-semantics using pure order-theoretic concepts only. As far as the systematic refinement operators on abstract domains are concerned, we show that uniform closures capture precisely the property of a refinement of being invertible, namely of admitting a related operator that simplifies as much as possible a given abstract domain of input for that refinement. Exploiting the same argument used to reconstruct the s-semantics of logic programming, we yield a precise relationship between refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.