Modular specification and verification of object-oriented programs

A method for modular specification and verification using the ideas of subtype and normal type is presented. The method corresponds to informal techniques used by object-oriented programmers. The key idea is that objects of a subtype must behave like objects of that type's supertypes. An example program is used to show the reasoning problems that supertype abstraction may cause and how the method resolves them. Subtype polymorphism is addressed, and specification and verification update is discussed. A set of syntactic and semantic constraints on subtype relationships, which formalize the intuition that each object of a subtype must behave like some object of each of its supertypes, is examined. These constraints are the key to the soundness of the method. To state them precisely, a formal model of abstract type specifications is used     

When does abstraction help?

Abstraction is a leading technique for coping with large state spaces. Abstraction over-approximates the transitions of the original system or the automaton that models it and may introduce nondeterminism. In applications where determinism is essential, we say that an abstraction function is helpful if, after determining and minimizing the abstract automaton, we end up with fewer states than the original automaton. We show that abstraction functions are not always helpful; in fact, they may introduce an exponential blow-up. We study the problem of deciding whether a given abstraction function is helpful for a given deterministic automaton and show that it is PSPACE-complete.     

面向未解释程序的合作验证方法

未解释程序的验证问题通常是不可判定的,但是最近有研究发现,存在一类满足coherence性质的未解释程序,其验证问题是可判定的,并且计算复杂度为PSPACE完全的.在这个结果的基础上,一个针对一般未解释程序验证的基于路径抽象的反例抽象精化（CEGAR）框架被提出,并展现了良好的验证效率.即使如此,对未解释程序的验证工作依然需要多次迭代,特别是利用该方法在针对多个程序验证时,不同的程序之间的验证过程是彼此独立的,存在验证开销巨大的问题.本文发现被验证的程序之间较为相似时,不可行路径的抽象模型可以在不同的程序之间复用.因此,本文提出了一个合作验证的框架,收集在验证过程中不可行路径的抽象模型,并在对新程序进行验证时,用已保存的抽象模型对程序进行精化,提前删减一些已验证的程序路径,从而提高验证效率.此外,本文通过对验证过程中的状态信息进行精简,对现有的基于状态等价的路径抽象方法进行优化,以进一步提升其泛化能力.本文对合作验证的框架以及路径抽象的优化方法进行了实现,并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速.     

Compositional verification of sequential programs with procedures

We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal μ-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.     

Verification Approach of Metropolis Design Framework for Embedded Systems

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate our approach for verification of system level designs at multiple levels of abstraction.     

Compositional Verification of Knowledge-Based Task Models and Problem-Solving Methods

In this paper a compositional verification method for task models and problem-solving methods for knowledge-based systems is introduced. Required properties of a system are formally verified by deriving them from assumptions that themselves are properties of sub-components, which in their turn may be derived from assumptions on sub-sub-components, and so on. The method is based on properties that are formalized in terms of temporal semantics; both static and dynamic properties are covered. The compositional verification method imposes structure on the verification process. Because of the possibility of focusing at one level of abstraction (information and process hiding), compositional verification provides transparency and limits the complexity per level. Since verification proofs are structured in a compositional manner, they can be reused in the event of reuse of models or modification of an existing system. The method is illustrated for a generic model for diagnostic reasoning.     

Aspects of abstraction in software development

Abstraction is a fundamental tool of human thought in every context. This essay briefly reviews some manifestations of abstraction in everyday life, in engineering and mathematics, and in software and system development. Vertical and horizontal abstraction are distinguished and characterised. The use of vertical abstraction in top-down and bottom-up program development is discussed, and also, the use of horizontal abstraction in one very different approach to program design. The ubiquitous use of analogical models in software is explained in terms of analytical abstractions. Some aspects of the practical use of abstraction in the development of computer-based systems are explored. The necessity of multiple abstractions is argued from the essential nature of abstraction, which by definition focuses on some concerns at the expense of discarding others. Finally, some general recommendations are offered for a consciously thoughtful use of abstraction in software development.     

基于软件模拟的SoC功能验证技术研究进展

软件模拟验证在SoC设计中得到了广泛的研究和应用,是目前SoC功能验证的主要方法.文中从高度抽象化、可重用和自动化三个方面梳理和综述了基于软件模拟的SoC功能验证技术的研究进展.同时,基于断言的验证在SoC的功能验证技术中起到重要的辅助性作用,文中阐述了断言技术的研究进展.最后,对软件模拟验证技术的发展趋势进行了展望.     

Abstraction-guided synthesis of synchronization

We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. Combined with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only the abstraction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be verified using the given abstraction. We implemented a prototype of our approach using numerical abstractions and applied it to verify several example programs.     

Counterexample-guided abstraction refinement for linear programs with arrays

Predicate abstraction refinement is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. Thus Boolean programs are commonly employed as a simple, yet useful abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. We present a novel counterexample guided abstraction refinement procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In our procedure the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the approaches based on predicate abstraction, our approach treats arrays precisely. This is an important feature as arrays are ubiquitous in programming. We provide a precise account of the abstraction, Model Checking, and refinement processes, discuss their implementation in the EUREKA tool, and present a detailed analysis of the experimental results confirming the effectiveness of our approach on a number of programs of interest.     

Lightweight Reasoning about Program Correctness

Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.     

A uniform presentation of confidentiality properties

Security (in the sense of confidentiality) properties are properties of shared systems. A suitable model of shared systems, in which one can formally define the term security property and then proceed to catalog several security properties, is presented. The purpose is to present various information-flow properties in a manner that exposes their differences and similarities. Abstraction is the main tool, and everything that is not central to the purpose is discarded. The presentation is generic in the model of computation. The abstraction lays bare a regular structure into which many interesting information-flow properties fall. A shared system is represented by a relation. How this model lets one reason about information flow is discussed and the term information flow property is formally defined. Various information-flow properties are described. Composability and probabilistic security properties are addressed     

一种C程序断言的全自动静态验证方法

在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足，从而使得验证过程可以终止。实验表明，提出的全自动静态断言验证方法不仅可行，而且验证代价较小，具有较强的实用性。     

Predicate Abstraction of ANSI-C Programs Using SAT

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relations of ANSI-C programs. The SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques.     

An Introduction to the Construction and Verification of Alphard Programs

The programming language Alphard is designed to provide support for both the methodologies of "well-structured" programming and the techniques of formal program verification. Language constructs allow a programmer to isolate an abstraction, specifying its behavior publicly while localizing knowledge about its implementation. The verification of such an abstraction consists of showing that its implementation behaves in accordance with its public specifications; the abstraction can then be used with confidence in constructing other programs, and the verification of that use employs only the public specifications.     

Dynamic verification of C++ generic algorithms

Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification one also needs to generate multiple program execution paths and use assertions (to handle while loops, for example), but the authors show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. They include an example of the formal verification of an STL generic algorithm     

Checking several requirements at once by CEGAR

Currently, static verifiers based on counterexample-guided abstraction refinement (CEGAR) can prove correctness of a program against a specified requirement, find its violation in a program, and stop analysis or exhaust the given resources without producing any useful result. Theoretically, we could use this approach for checking several requirements at once; however, finding of the first violation of some requirement or exhausting resources for some requirement will prevent from checking the program against other requirements. Moreover, if the program contains more than one violation of the requirement, CEGAR will find only the very first violation and may miss potential errors in the program. At the same time, static verifiers perform similar actions during checking of the same program against different requirements, which results in waste of a lot of resources. This paper presents a new CEGAR-based method for software static verification, which is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR checking requirements one by one. To achieve this goal, the suggested method distributes resources over requirements and continues analysis after finding a violation of a requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by five times. The total number of divergent results in comparison with the base CEGAR was about 2%. Having continued the analysis after finding the first violation, this method guarantees that all violations of given requirements are found in 40% of cases, with the number of violations found being 1.5 times greater than in that in the base CEGAR approach.     

Program verification,defeasible reasoning,and two views of computer science

In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing and formal verification do not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other.