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.     

Predicate abstraction in a program logic calculus

Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for deductive program verification based on symbolic execution, where it allows us to infer loop invariants automatically that would otherwise have to be given interactively. The approach has been implemented as a part of the KeY verification system.     

Code obfuscation against abstraction refinement attacks

Code protection technologies require anti reverse engineering transformations to obfuscate programs in such a way that tools and methods for program analysis become ineffective. We introduce the concept of model deformation inducing an effective code obfuscation against attacks performed by abstract model checking. This means complicating the model in such a way a high number of spurious traces are generated in any formal verification of the property to disclose about the system under attack.We transform the program model in order to make the removal of spurious counterexamples by abstraction refinement maximally inefficient. Because our approach is intended to defeat the fundamental abstraction refinement strategy, we are independent from the specific attack carried out by abstract model checking. A measure of the quality of the obfuscation obtained by model deformation is given together with a corresponding best obfuscation strategy for abstract model checking based on partition refinement.     

Encoding, Decoding and Data Refinement

Data refinement is the systematic replacement of a data structure with another one in program development. Data refinement between program statements can on an abstract level be described as a commutativity property where the abstraction relationship between the data structures involved is represented by an abstract statement (a decoding). We generalise the traditional notion of data refinement by defining an encoding operator that describes the least (most abstract) data refinement with respect to a given abstraction. We investigate the categorical and algebraic properties of encoding and describe a number of special cases, which include traditional notions of data refinement. The dual operator of encoding is decoding, which we investigate and give an intuitive interpretation to. Finally we show a number of applications of encoding and decoding. Received May 1999 / Accepted in revised form November 2000     

Verification and falsification of programs with loops using predicate abstraction

Predicate abstraction is a major abstraction technique for the verification of software. Data is abstracted by means of Boolean variables, which keep track of predicates over the data. In many cases, predicate abstraction suffers from the need for at least one predicate for each iteration of a loop construct in the program. We propose to extract looping counterexamples from the abstract model, and to parametrise the simulation instance in the number of loop iterations. We present a novel technique that speeds up the detection of long counterexamples as well as the verification of programs with loops.     

Program translation via abstraction and reimplementation

An abstraction-and-reimplementation paradigm is presented in which the source program is first analyzed in order to obtain a programming-language-independent abstract understanding of the computation performed by the program as a whole. The program is then reimplemented in the target language based on this understanding. The key to this approach is the abstract understanding obtained. It allows the translator to benefit from an appreciation of the global features of the source program without being distracted by what are considered irrelevant details. Knowledge-based translation via abstraction and reimplementation is described as one of the goals of the Programmer's Apprentice project. A translator which translates Cobol programs into Hibol (a very-high-level business data processing language) has been constructed. A computer which generates extremely efficient PDP-11 object code for Pascal programs has been designed     

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

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

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.     

QDA-a method for systematic informal program analysis

Formal verification of program properties may be infeasible or impractical, and informal analysis may be sufficient. Informal analysis involves the informal acceptance, by inspection, of the validity of program properties or steps in an analysis. Informal analysis may also involve abstraction. Abstraction can be used to eliminate details and concentrate on more general properties. Abstraction will result in informal analysis if it includes the use of undefined properties. A systematic, informal method for analysis called QDA (Quick Defect Analysis) is described. QDA is a comments analysis process based on facts and hypotheses. Facts are used to create an abstract program model, and hypotheses are selected, nonobvious program properties which are identified as needing verification. Hypotheses are proved from the facts that define an abstraction. QDA is hypothesis-driven in the sense that only those parts of an abstraction that are needed to prove hypotheses are created. The QDA approach was applied to a previously well tested operational flight program (OFP). The QDA method and the results of the OFP experiment are presented. The problems of incomplete or unsound informal analysis are analyzed, the relationship of QDA to other analysis methods is discussed, and suggested improvements to the QDA method are described     

Loop summarization using state and transition invariants

This paper presents algorithms for program abstraction based on the principle of loop summarization, which, unlike traditional program approximation approaches (e.g., abstract interpretation), does not employ iterative fixpoint computation, but instead computes symbolic abstract transformers with respect to a set of abstract domains. This allows for an effective exploitation of problem-specific abstract domains for summarization and, as a consequence, the precision of an abstract model may be tailored to specific verification needs. Furthermore, we extend the concept of loop summarization to incorporate relational abstract domains to enable the discovery of transition invariants, which are subsequently used to prove termination of programs. Well-foundedness of the discovered transition invariants is ensured either by a separate decision procedure call or by using abstract domains that are well-founded by construction. We experimentally evaluate several abstract domains related to memory operations to detect buffer overflow problems. Also, our light-weight termination analysis is demonstrated to be effective on a wide range of benchmarks, including OS device drivers.     

Experience with Abstraction-carrying Code

Abstraction-carrying Code (ACC) certifies a general temporal property for a mobile program using an abstract interpretation of the mobile program. A client receiving the code and the certificate will first validate the abstraction and then run a model checker to verify the temporal property.In this paper, we report our experience in designing the ACC Evaluation Prototype Toolkit (ACCEPT) and the application of ACCEPT to simple concurrent programs and Linux device drivers. The toolkit is distinguished by an abstraction preserving compilation scheme that generates a Boolean program for an intermediate program compiled from the source program. Some common compiler optimizations are still possible. We report several applications of ACCEPT, including the reachability properties of industrial strength C programs. Preliminary results show that the size of a typical certificate is significantly smaller than the size of the intermediate program. Compared with traditional proof-based certification method, using ACC verification a client spends more time to verify the desired property. Our experience shows this penalty is often tolerable in practice.     

程序变换在程序语言中的一种表示——兼论变换型语言

本文首先引入了“变换型语言”的概念,给出了代表这种语言特征的机制:“变换模块”和“变换控制命令”的具体定义;举例说明了如何使用“变换模块”描述一个抽象数据类型的部分实现,并通过“变换控制命令”来完成程序中抽象变量及有关操作的变换过程;最后,讨论了变换型语言表示的抽象性,一般性和控制的灵活性,以及变换型程序的正确性等问题。     

Abstractions of data types

The use of abstraction in the context of abstract data types, is investigated. Properties to be checked are formulas in a first order logic under Kleene's 3-valued interpretation. Abstractions are defined as pairs consisting of a congruence and a predicate interpretation. Three types of abstractions are considered,∀∀, ∀∃ and ∃^0,1∀, and for each of them corresponding property preservation results are established. An abstraction refinement property is also obtained. It shows how one can pass from an existing abstraction to a (less) finer one. Finally, equationally specified abstractions in the context of equationally specified abstract data types are discussed and exemplified.On leave from the Department of Computer Science, “Al. I. Cuza” University, Iaşi 740083, RomaniaThe research reported in this paper was partially supported by the program ECO-NET 08112WJ/2004-2005 and by the National University Research Council of Romania, grants CNCSIS 632(28)/2004 and CNCSIS 632(50)/2005.     

Non-Standard Semantics for Program Slicing

In this paper we generalize the notion of compositional semantics to cope with transfinite reductions of a transition system. Standard denotational and predicate transformer semantics, even though compositional, provide inadequate models for some known program manipulation techniques. We are interested in the systematic design of extended compositional semantics, observing possible transfinite computations, i.e. computations that may occur after a given number of infinite loops. This generalization is necessary to deal with program manipulation techniques modifying the termination status of programs, such as program slicing. We include the transfinite generalization of semantics in the hierarchy developed in 1997 by P. Cousot, where semantics at different levels of abstraction are related with each other by abstract interpretation. We prove that a specular hierarchy of non-standard semantics modeling transfinite computations of programs can be specifiedin such a way that the standard hierarchy can be derived by abstract interpretation. We prove that non-standard transfinite denotational and predicate transformer semantics can be both systematically derived as solutions of simple abstract domain equations involving the basic operation of reduced power of abstract domains. This allows us to prove the optimality of these semantics, i.e. they are the most abstract semantics in the hierarchy which are compositional and observe respectively the terminating and initial states of transfinite computations, providing an adequate mathematical model for program manipulation.     

Type Transformations

Current work on data structure encapsulation and abstraction focuses attention on individual structures and permits separate local optimizations, of these structures. We extend this work by developing the beginnings of an algebra for aggregating individual data types into larger more coordinated structures which can be more effectively optimized. The present work can well be viewed as the data equivalent of cross-procedural optimization. We believe aggregations of pure abstract types are both common and essential in practical programs and that techniques for building and manipulating them must be developed before abstract specification and program transformation can become a practical programming paradigm.     

High-Level Views of Distributed Executions: Convex Abstract Events

Due to the complexity of distributed applications, understanding their behaviour is a challenging task. To remedy this problem, graphical visualizations of distributed executions in the form of process-time diagrams are frequently employed. However, such process-time diagrams do not scale for long-running and complex distributed applications. To reduce the display complexity, abstract graphical views of an execution are frequently suggested. One commonly used abstraction is to group primitive events into abstract events. This paper discusses some of the problems encountered when analyzing executions at abstract levels and introduces the concept of convex abstract events. Such abstract events can be used to reason about executions at higher levels, facilitating program development, debugging, and maintenance. We discuss some fundamental aspects, such as the precedence relation and its efficient detection, for abstract events. The paper also presents a graphical representation for convex abstract events which can easily be included in process-time diagrams. Poet, our visualization tool, was enhanced with a facility to display abstract events. Using a non-trivial distributed application, examples of the resulting abstract execution visualizations are discussed.     

IPTV点播业务中减少特技播放交互延迟的方法

优化交互响应时间是提高IPTV用户体验质量（QoE）的重要措施。为了减少特技播放过程的交互延迟,提出对媒体随机访问点建立索引的方法,以便媒体服务器通过查找索引表即可实现随机访问点的快速定位和关键帧提取。通过对MPEG-2 TS流的系统层结构和H.264 NAL层的结构分析,探讨了封装H.264视频的TS格式媒体文件的两种关键帧提取方法。鉴于IPTV媒体服务器存储的媒体文件数量庞大,采用Hash的方法建立节目信息索引表,以提高节目信息查找效率。最后给出了在媒体预处理过程中为点播内容建立节目信息索引表和随机访问点索引表以减少IPTV特技播放交互延迟的具体实现方案。方案可行性在与华为合作开发的IMS-based IPTV原型系统得到了验证,测试结果符合三重播放业务QoE的交互响应时间要求。     

Abstraction-Carrying Code: a Model for Mobile Code Safety

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the “untrusted” program by means of a certificate checker—a process which should be much simpler, efficient, and automatic than generating the original proof. The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both proving programs correct and replacing a costly verification process by an efficient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on the consumer side is checked in a single pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety.

---

     

Toward formal development of programs from algebraic specifications: Implementations revisited

Summary The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction “on top of” the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results are shown to generalise to the framework of an arbitrary institution, and a way of changing institutions during the implementation process is introduced. All this is illustrated by means of simple concrete examples. An extended abstract of this paper appeared in [65].     

Linking Unifying Theories of Program refinement

In this paper we consider three theories of programs and specifications at different levels of abstraction. The theories we focus on are: the basic Unifying Theories of Programming (UTP) model, which corresponds to the theories of VDM, B, and the refinement calculus; an extended theory that distinguishes abort from nontermination; and a further extension that introduces (abstract) time. We define UTP-style designs (or specifications) in each theory and show how program constructors, such as nondeterministic choice and sequential composition, can be expressed as single designs in each theory.