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.     

The potential of Swetra — A multilanguage MT system

One may indicate the potentials of an MT system by stating what text genres it can process, e.g., weather reports and technical manuals. This approach is practical, but misleading, unless domain knowledge is highly integrated in the system. Another way to indicate which fragments of language the system can process is to state its grammatical potentials, or more formally, which languages the grammars of the system can generate. This approach is more technical and less understandable to the layman (customer), but it is less misleading, since it stresses the point that the fragments which can be translated by the grammars of a system need not necessarily coincide exactly with any particular genre. Generally, the syntactic and lexical rules of an MT system allow it to translate many sentences other than those belonging to a certain genre. On the other hand it probably cannot translate all the sentences of a particular genre. Swetra is a multilanguage MT system defined by the potentials of a formal grammar (standard referent grammar) and not by reference to a genre. Successful translation of sentences can be guaranteed if they are within a specified syntactic format based on a specified lexicon. The paper discusses the consequences of this approach (Grammatically Restricted Machine Translation, GRMT) and describes the limits set by a standard choice of grammatical rules for sentences and clauses, noun phrases, verb phrases, sentence adverbials, etc. Such rules have been set up for English, Swedish and Russian, mainly on the basis of familiarity (frequency) and computer efficiency, but restricting the grammar and making it suitable for several languages poses many problems for optimization. Sample texts — newspaper reports — illustrate the type of text that can be translated with reasonable success among Russian, English and Swedish.     

The potential of swetra—A multilanguage MT system

One may indicate the potentials of an MT system by stating what text genres it can process, e.g., weather reports and technical manuals. This approach is practical, but misleading, unless domain knowledge is highly integrated in the system. Another way to indicate which fragments of language the system can process is to state its grammatical potentials, or more formally, which languages the grammars of the system can generate. This approach is more technical and less understandable to the layman (customer), but it is less misleading, since it stresses the point that the fragments which can be translated by the grammars of a system need not necessarily coincide exactly with any particular genre. Generally, the syntactic and lexical rules of an MT system allow it to translate many sentences other than those belonging to a certain genre. On the other hand it probably cannot translate all the sentences of a particular genre. Swetra is a multilanguage MT system defined by the potentials of a formal grammar (standard referent grammar) and not by reference to a genre. Successful translation of sentences can be guaranteed if they are within a specified syntactic format based on a specified lexicon. The paper discusses the consequences of this approach (Grammatically Restricted Machine Translation, GRMT) and describes the limits set by a standard choice of grammatical rules for sentences and clauses, noun phrases, verb phrases, sentence adverbials, etc. Such rules have been set up for English, Swedish and Russian, mainly on the basis of familiarity (frequency) and computer efficiency, but restricting the grammar and making it suitable for several languages poses many problems for optimization. Sample texts—newspaper reports—illustrate the type of text that can be translated with reasonable success among Russian, English and Swedish.     

C program verification: Verification condition explanation and standard library

Two lines of developing the C program verification project at the A.P. Ershov Institute of Informatic Systems are presented. Firstly, the axiomatic semantics of the C-kernel language was extended by the semantic labelling. The labels introduced in the Hoare calculus correspond to various concepts inherent in verification conditions (VC). These labels can be extracted from terms and rendered into explanations written in the natural language. User friendly explanations can play a crucial role in VC understanding and error localization. Secondly, a subset of the C standard library was specified. The specifications written in ACSL correspond to the C-light memory model. Examples illustrating the use of the proposed techniques are presented.     

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.     

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.     

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.     

一种验证指针程序的方法

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

并行程序验证的调度策略

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

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).     

Recent advances in program verification through computer algebra

In this paper, we summarize the results on program verification through semi-algebraic systemsSASs 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.     

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.     

VerifyThis 2019: a program verification competition

VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

     

随机测试程序生成器研究

随机测试是微处理器设计过程的重要环节,按照一定原则生成的随机指令序列,能够构造出指令组合的各种情况,达到比较好的测试强度和较高的覆盖率。介绍了一种基于模拟器的动态随机测试程序生成器的实现机制,此生成器用多个状态机来抽象整个被测处理器的可能行为,具有简单和高效的特点。给出了测试的统计数据。随机测试生成器对清华大学具有自主知识产权的微处理器的测试过程中取得了良好的测试效果。     

Towards a transformational approach to program verification

Although most typically used in other contexts, program transformations can simplify program verification by transforming a program containing complex language features into a semantically equivalent program containing only simpler language features. The proof of the transformed program can then be performed using a set of proof rules for only the simpler features. There are tradeoffs between the transformational approach and the standard approach to program verification with regard to proof understandability and compactness of programs and assertions, establishing soundness of the program verification method, and providing mechanized support for the method. The transformational approach has clear advantages in some of these aspects. This paper illustrates this transformational approach by considering proof rules for escape statements in iterative constructs, and discusses the tradeoffs with respect to its use. It also suggests how the approach can be applied to other language constructs, including some involving concurrency, and to solving some problems connected with the development of Hoare axiomatizations. Copyright © 1999 John Wiley & Sons, Ltd.