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.     

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.     

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.     

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.     

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.     

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.     

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.     

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.     

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

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

Expressive program verification via structured specifications

Conventional specifications typically have a flat structure that is based primarily on the underlying logic. Such specifications lack structures that could provide better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control over the verification process in the following ways: (1) case analysis can be invoked to take advantage of disjointedness conditions in the logic, (2) early, as opposed to late, instantiation can minimise the use of existential quantification and (3) novel formulae structuring can provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead. To support our proposal, we shall illustrate the usage of structured specifications in the context of proving termination and we will briefly outline the impact of our proposal on a recent development focussed on verifying the FreeRTOS scheduler Ferreira et al. (Int. J. Softw. Tools Technol. Trans. 2014).     

一种验证指针程序的方法

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

Recent advances in program verification through computer algebra

In this paper, we summarize the results on program verification through semi-algebraic systems (SASs) solving that we have obtained, including automatic discovery of invariants and ranking functions, symbolic decision procedure for the termination of a class of linear loops, termination analysis of nonlinear systems, and so on.     

Attribute annotations and their use in C program deductive verification

In this paper, a new kind of annotations called attribute annotations and the methodology for their application in deductive program verification are proposed. A collection of annotating attributes for the C-kernel subset of the C language is described, and, on their basis, two versions of axiomatic semantics of C-kernel—forward semantics and mixed forward semantics—are presented.     

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols

Narrowing was introduced, and has traditionally been used, to solve equations in initial and free algebras modulo a set of equations E. This paper proposes a generalization of narrowing which can be used to solve reachability goals in initial and free models of a rewrite theory ?. We show that narrowing is sound and weakly complete (i.e., complete for normalized solutions) under appropriate executability assumptions about ?. We also show that in general narrowing is not strongly complete, that is, not complete when some solutions can be further rewritten by ?. We then identify several large classes of rewrite theories, covering many practical applications, for which narrowing is strongly complete. Finally, we illustrate an application of narrowing to analysis of cryptographic protocols.     

A new order relation on fuzzy soft sets and its application

In this paper, a new order relation on fuzzy soft sets, called soft information order, is introduced and its application to decision-making is investigated. It is shown that the collection of all fuzzy soft sets (over a given universe set), equipped with this new order, forms a complete Heyting algebra. The representation theorem of fuzzy soft sets with respect to the soft information order is also obtained. We initiate the concepts of soft set satisfaction problems and their solutions. An algorithm is presented to solve such decision-making problems.