Template-based program verification and program synthesis

Program verification is the task of automatically generating proofs for a program’s compliance with a given specification. Program synthesis is the task of automatically generating a program that meets a given specification. Both program verification and program synthesis can be viewed as search problems, for proofs and programs, respectively. For these search problems, we present approaches based on user-provided insights in the form of templates. Templates are hints about the syntactic forms of the invariants and programs, and help guide the search for solutions. We show how to reduce the template-based search problem to satisfiability solving, which permits the use of off-the-shelf solvers to efficiently explore the search space. Template-based approaches have allowed us to verify and synthesize programs outside the abilities of previous verifiers and synthesizers. Our approach can verify and synthesize difficult algorithmic textbook programs (e.g., sorting and dynamic programming-based algorithms) and difficult arithmetic programs.     

Automatic program verification I: A logical basis and its implementation

Summary Defining the semantics of programming languages by axioms and rules of inference yields a deduction system within which proofs may be given that programs satisfy specifications. The deduction system herein is shown to be consistent and also deduction complete with respect to Hoare's system. A subgoaler for the deduction system is described whose input is a significant subset of Pascal programs plus inductive assertions. The output is a set of verification conditions or lemmas to be proved. Several non-trivial arithmetic and sorting programs have been shown to satisfy specifications by using an interactive theorem prover to automatically generate proofs of the verification conditions. Additional components for a more powerful verification system are under construction.This research is supported by the Advanced Research Projects Agency under Contracts SD-183 and DAHC 15-72-C-0308, and by the National Aeronautics and Space Administration under Contract NSR 05-020-500.     

非经典切片技术及其在形式验证中的应用综述

切片技术最初是作为一种程序分解抽取的分析技术而出现的,经过20多年的不断发展和完善,应用范围已遍及软件工程学科的各个方面。特别是从本世纪初,随着非经典切片：计算切片和证明切片两个新兴研究方向的出现,其学术研究和工程价值越发突出。简要地介绍了切片技术思想的起源、发展过程,并着重介绍非经典的计算切片和证明切片技术及其在验证领域的应用。     

Experiments in program verification using Event-B

The Event-B method can be used to model all sorts of discrete event systems, among them sequential programs. In this article we describe our experiences with using Event-B by way of two examples. We present a simple model of a factorial program, explaining the method, and a more intricate model of the Quicksort algorithm, providing some insights into strengths and weaknesses of Event-B. The two models are interspersed with our observations and some suggestions of how, we believe, Event-B could evolve. This evaluation of Event-B is intended to serve for determining directions for the evolution of Event-B and judging progress. It is our hope that the observations and suggestions can also be put to use for similar modelling formalisms, such as Z, ASM or VDM.     

ACTL strong negation and its application to hybrid systems verification

Model checking procedures for verifying properties of hybrid dynamic systems are based on the construction of finite-state abstractions. If the property is not satisfied by the abstraction, the verification is inconclusive and the abstraction needs to be refined so that a less conservative model can be checked. If the hybrid system does not satisfy the property, this verify–refine procedure usually will not terminate. This paper introduces the concept of strong negation for ACTL formulas as an auxiliary condition that can be verified to obtain a conclusive negative verification result from a finite-state abstraction in certain cases. The concepts are illustrated with an example from automotive powertrain control.     

An executable object-oriented semantics and its application to firewall verification

This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system.     

曲线弯曲多叉树模型及其在地图综合中的应用

针对曲线弯曲二叉树在曲线形态表达上的不足,以弯曲作为曲线形态的单元,探讨了曲线的多尺度表达与弯曲树状结构间的关系,提出了曲线的弯曲多叉树模型以及探测方法,并利用曲线弯曲多叉树模型制定了基于弯曲的曲线综合化简策略。该模型在等高线化简上的应用表明,其无论在线要素的整体形态保持上,还是在地理特征的一致性保持上都非常有效。     

GM(1,1)模型拓广方法研究与应用

为了拓广GM(1,1)模型的适用范围,对GM(1,1)模型进行了两方面的改进:对初始序列进行预处理以改善其光滑性;用GM(1,1)模型的内涵型代替白化响应式作为新的预测公式.理论分析与实验结果表明,改进模型不仅比传统模型的预测精度高,而且完全适用干对高增长序列建模,拓广了GM(1,1)模型的适用范围.     

Philosophical aspects of program verification

A debate over the theoretical capabilities of formal methods in computer science has raged for more than two years now. The function of this paper is to summarize the key elements of this debate and to respond to important criticisms others have advanced by placing these issues within a broader context of philosophical considerations about the nature of hardware and of software and about the kinds of knowledge that we have the capacity to acquire concerning their performance.     

A generalization of frame perturbation in Hilbert subspaces and its application to wavelet subspaces

A perturbation theorem for frames in a Hilbert space is obtained, which is a generalization of a result by Christensen. Based on this general result, an irregular sampling theorem for frames in wavelet subspaces is established, which has a previous result as a special case.     

Formal verification technique for grid service chain model and its application

Ensuring the correctness and reliability of large-scale resource sharing and complex job processing is an important task for grid applications. From a formal method perspective, a grid service chain model based on state Pi calculus is pro- posed in this work as the theoretical foundation for the service composition and collaboration in grid. Following the idea of the Web Service Resource Framework (WSRF), state Pi calculus enables the life-cycle management of system states by associating the actions in the original Pi calculus with system states. Moreover, model checking technique is exploited for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effective- ness of the proposed work.     

C program verification in SPECTRUM multilanguage system

An extendable multilanguage analysis and verification system SPECTRUM is presented; this system is being developed in the framework of the project SPECTRUM. The prospects of the application of this system are demonstrated, as exemplified by the verification of C programs. The project SPECTRUM is aimed at the creation of a new integrated approach to the verification of imperative programs that makes it possible to integrate, unify, and combine methods and approaches for verification of imperative programs and accumulate and apply information about these programs. The specific feature of this approach is the application of a specialized executable specification language Atoment for the development of program verification tools; this language makes it possible to represent methods and approaches for verification and data for them (program models, annotations, logical formulae) in a unified format. The C component of the SPECTRUM system uses a two-level C program verification method. This method is a good illustration of the integrated approach, since it provides complex verification of C programs based on a combination of the operational, axiomatic, and transformational approaches.     

二阶锥规划在MR图像重建中的应用研究

用传统MR图像重建方法对降采样数据进行重建往往会产生严重的伪影或导致重建图像的信噪比下降。用迭代重建算法对MR降采样数据进行优质重建,目标函数仅包含待重建图像的全变分,约束条件为一等式约束。在数值求解过程中,将优化问题转化为二阶锥规划问题,采用具有良好收敛性的对数障碍算法进行优化求解。在迭代过程中用图像的全变分信息自适应地决定对数障碍参数。实验结果表明,算法很好地克服了网格算法中的伪影问题,可以重建出高质量的MR图像。     

基于混沌序列的SVM参数选择及其在笔迹鉴别中的应用

基于RBF核的支持向量机(SVM)模型选择取决于两个参数，即惩罚因子和核参数，为了寻找SVM参数的最优组合，利于笔迹鉴别图像的自动识别，提出了基于混沌序列的参数搜索算法以实现SVM模型参数的自动选择。从与网格法和双线性法进行的比较实验可以看出，基于混沌序列的SVM参数选取更简单，更易于实现，并使SVM具有更好的推广能力。在10人笔迹灰度图像库上分类识别实验结果表明，该方法不但可以提高分类识别率，而且显著减少了训练SVM的个数。     

基于专家知识的字典序优化决策方法及工业应用

为有效实现有色冶金配料过程的实时优化,首先根据氧化铝配料过程特点,建立一种字典序区间目标规划模型;然后通过整理长期积累的专家经验知识,构建了具有优先级的分类知识库;接着基于专家知识库的分类结构,提出一种字典序专家推理策略,以实现区间约束条件下的多质量指标的优化控制．工业应用结果表明,所提出的方法能够很好地实现生料浆质量的优化控制,为其他有色冶金工业配料过程的控制提供了一种优化模式．     

一种验证指针程序的方法

利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下,避免在Hoare逻辑上做复杂扩展的指针程序验证方法。

Abstract：

Analysis and verification of programs dealing with pointers are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems. Using our method, programmers must declare the shapes that the recursive data     

并行程序验证的调度策略

针对形式化程序验证中的并行调度问题,提出了基于依赖集的算法。通过引入依赖图和依赖集概念,以形式化方式描述程序语句间的依赖关系,然后给出了从语法分析树构造依赖图和依赖集的算法;最后在此基础上设计了并行调度算法并应用于计算机辅助程序验证系统。实验结果表明,该方法具有较高的并行效率。