PAR方法和循环不变式的范畴语义

范畴论对理解程序规约及程序设计和正确性证明十分有用。PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法。循环不变式在循环算法程序的设计中至关重要。使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础。在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程。     

On software verification for sensor nodes

We consider software written for networked, wireless sensor nodes, and specialize software verification techniques for standard C programs in order to locate programming errors in sensor applications before the software's deployment on motes. Ensuring the reliability of sensor applications is challenging: low-level, interrupt-driven code runs without memory protection in dynamic environments. The difficulties lie with (i) being able to automatically extract standard C models out of the particular flavours of embedded C used in sensor programming solutions, and (ii) decreasing the resulting program's state space to a degree that allows practical verification times.We contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 embedded C with asynchronous hardware interrupts. Our tool automatically translates the program into standard C by modelling the MCU's memory map and direct memory access. To emulate the existence of hardware interrupts, calls to hardware interrupt handlers are added, and their occurrence is minimized with a double strategy: a partial-order reduction technique, and a supplementary reachability check to reduce overapproximation. This decreases the program's state space, while preserving program semantics. Safety specifications are written as C assertions embedded in the code. The resulting sequential program is then passed to CBMC, a bounded software verifier for sequential ANSI C. Besides standard errors (e.g., out-of-bounds arrays, null-pointer dereferences), this tool chain is able to verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.Verification for wireless sensor network applications is an emerging field of research; thus, as a final note, we survey current research on the topic.     

Automated Verification of Functional Correctness of Race-Free GPU Programs

We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop invariants, and passes them to off-the-shelf SMT solvers. It is often impossible, however, to solve naively generated VCs in reasonable time. A main difficulty stems from quantifiers over threads due to the parallel nature of GPU programs. To overcome this difficulty, we additionally apply several transformations to simplify VCs before calling SMT solvers. Our implementation successfully verifies correctness of several GPU programs, including matrix multiplication optimized by using shared memory. In contrast to many existing verification tools for GPU programs, our verifier succeeds in verifying fully parameterized programs: parameters such as the number of threads and the sizes of matrices are all symbolic. We empirically confirm that our simplification heuristics is highly effective for improving efficiency of the verification procedure.     

Dynamically discovering likely program invariants to supportprogram evolution

Explicitly stated program invariants can help programmers by identifying program properties that must be preserved when modifying code. In practice, however, these invariants are usually implicit. An alternative to expecting programmers to fully annotate code with invariants is to automatically infer likely invariants from the program itself. This research focuses on dynamic techniques for discovering invariants from execution traces. This article reports three results. First, it describes techniques for dynamically discovering invariants, along with an implementation, named Daikon, that embodies these techniques. Second, it reports on the application of Daikon to two sets of target programs. In programs from Gries's work (1981) on program derivation, the system rediscovered predefined invariants. In a C program lacking explicit invariants, the system discovered invariants that assisted a software evolution task. These experiments demonstrate that, at least for small programs, invariant inference is both accurate and useful. Third, it analyzes scalability issues, such as invariant detection runtime and accuracy, as functions of test suites and program points instrumented     

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.     

命令式动态规划类算法程序推导及机械化验证

动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.     

程序不变量检测技术

基于合约的程序设计是提高软件质量的一种重要技术,已经得到了很大的发展。合约描述了程序内部的基本属性、程序良性运行的保证条件以及运行后的期望结果。作为合约的一种表达形式,程序不变量一般包含类不变量、前置条件和后置条件。程序不变量是程序中隐含的属性,它可以应用于程序验证、软件测试技术、逆向工程、程序质量保证等领域。本文结合当前主流的程序不变量研究的相关成果和基于合约的程序不变量程序设计方法,分别从源程序编配技术、测试用例生成技术、程序运行轨迹收集技术和程序不变量分析技术四个方面,对程序不变量挖掘的关键方法和原理进行了详细的剖析。     

CILinear:一个线性不变式自动构造工具

构造不变式是程序验证的重要组成部分,而开源工具Interpro。能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CII,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了CILinear在程序验证中的实际应用。     

Automata-based verification of programs with tree updates

This paper describes a verification framework for Hoare-style pre- and post-conditions of programs manipulating balanced tree-like data structures. Since the considered verification problem is undecidable, we appeal to the standard semi-algorithmic approach in which the user has to provide loop invariants, which are then automatically checked, together with the program pre- and post-conditions. We specify sets of program states, representing tree-like memory configurations, using Tree Automata with Size Constraints (TASC). The main advantage of this new class of tree automata is that they recognise tree languages based on arithmetic reasoning about the lengths of various (possibly all) paths in trees, like, e.g., in AVL trees or red–black trees. TASCs are closed under union, intersection, and complement, and their emptiness problem is decidable. Thus we obtain a class of automata which are an interesting theoretical contribution by itself. Further, we show that, under few restrictions, one can automatically compute the effect of tree-updating program statements on the set of configurations represented by a TASC, which makes TASC a practical verification tool. We tried out our approach on the insertion procedure for red–black trees, for which we verified that the output on an arbitrary balanced red–black tree is also a balanced red–black tree.     

Scenario-based and value-based specification mining: better together

Specification mining takes execution traces as input and extracts likely program invariants, which can be used for comprehension, verification, and evolution related tasks. In this work we integrate scenario-based specification mining, which uses a data-mining algorithm to suggest ordering constraints in the form of live sequence charts, an inter-object, visual, modal, scenario-based specification language, with mining of value-based invariants, which detects likely invariants holding at specific program points. The key to the integration is a technique we call scenario-based slicing, running on top of the mining algorithms to distinguish the scenario-specific invariants from the general ones. The resulting suggested specifications are rich, consisting of modal scenarios annotated with scenario-specific value-based invariants, referring to event parameters and participating object properties. We have implemented the mining algorithm and the visual presentation of the mined scenarios within a standard development environment. An evaluation of our work over a number of case studies shows promising results in extracting expressive specifications from real programs, which could not be extracted previously. The more expressive the mined specifications, the higher their potential to support program comprehension and testing.     

Provably correct derivation of algorithms using FermaT

The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate “verification” step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.     

基于QBF的循环不变式构造技术

构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然。针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。     

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.     

Mechanical inference of invariants for FOR-loops

In the mechanical verification of programs containing loops it is often necessary to provide loop invariants additionally to the specification in the form of pre and postconditions. In this paper we present a method for the mechanical inference of invariants for a practically relevant class of FOR-loops. The invariant is derived from the specification (pre, post) and the final bound of the loop only. The method is based on the technique “replacing a constant in post by a variable”, which has traditionally been used manually for the development of WHILE-loops. Our method is a complete mechanization of this heuristic for the verification of existing annotated FOR-loops. The range of applicability of the method is further extended by a technique called “bound transformation” and by taking common invariant conjuncts of pre and post into account. As a result, the method is applicable to the majority of FOR-loops occurring in practice.     

Unified Approach for Developing EfficientAlgorithmic Programs

A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented.An algorithm(represented by recurrence and initiation)is separated from program,and special attention is paid to algorithm manipulation rather than proram calculus.An algorithm is exactly a set of mathematical formulae.It is easier for formal erivation and proof.After getting efficient and correct algorithm,a trivial transformation is used to get a final rogram,The approach covers several known algorithm design techniques,e.g.dynamic programming,greedy,divide-and-conquer and enumeration,etc.The techniques of partition and recurrence are not new.Partition is a general approach for dealing with complicated objects and is typically used in divide-and-conquer approach.Recurrence is used in algorithm analysis,in developing loop invariants and dynamic programming approach.The main contribution is combining two techniques used in typical algorithm development into a unified and systematic approach to develop general efficient algorithmic programs and presenting a new representation of algorithm that is easier for understanding and demonstrating the correctness and ingenuity of algorithmicprograms.     

利用基因表达式编程自动生成循环不变式

描述了利用基因表达式编程自动生成循环不变式的方法。该方法的基本思想是在每一次循环条件变化时记录下程序变量的值,产生相应的跟踪表,然后从跟踪表中获得程序变量之间的函数依赖关系,这种变量之间的依赖关系构成了循环不变式的主要部分。程序变量之间的函数依赖关系的获得是利用基因表达式编程对跟踪表中数据执行符号回归得到。利用VC＋＋实现了基因表达式编程的函数挖掘,并通过一个实例说明了该方法的有效性。     

Validating numerical semidefinite programming solvers for polynomial invariants

Semidefinite programming (SDP) solvers are increasingly used as primitives in many program verification tasks to synthesize and verify polynomial invariants for a variety of systems including programs, hybrid systems and stochastic models. On one hand, they provide a tractable alternative to reasoning about semi-algebraic constraints. However, the results are often unreliable due to “numerical issues” that include a large number of reasons such as floating-point errors, ill-conditioned problems, failure of strict feasibility, and more generally, the specifics of the algorithms used to solve SDPs. These issues influence whether the final numerical results are trustworthy or not. In this paper, we briefly survey the emerging use of SDP solvers in the static analysis community. We report on the perils of using SDP solvers for common invariant synthesis tasks, characterizing the common failures that can lead to unreliable answers. Next, we demonstrate existing tools for guaranteed semidefinite programming that often prove inadequate to our needs. Finally, we present a solution for verified semidefinite programming that can be used to check the reliability of the solution output by the solver and a padding procedure that can check the presence of a feasible nearby solution to the one output by the solver. We report on some successful preliminary experiments involving our padding procedure.     

Temporal logic programming for assembly sequence planning

A temporal-constraint logic programming framework for the specification and automatic verification and synthesis of assembly sequences is developed. The implemented tool is based on the formulated and derived precedence properties for a general mechanical assembly. This tool, called the Mechanical Assembly Sequence Satisfiability Checker (MASS-C), supports the use of a subset of temporal logic for assembly constraint specification. MASS-C provides the logic programming framework by which the designer can be relieved of the tedium of finding the assembly sequences, and the assembly sequence planning process manifests itself in the implicit modelling of assembly sequences by acquiring and formulating the set of correct and complete assembly constraints as a logic program. MASS-C implements a class of temporal expressions as predicates for logic programming of assembly constraints. It provides facilities to either verify an assembly sequence or synthesise all assembly sequences that satisfy the specified constraints composed as a logic program. Two examples illustrate the use of MASS-C for such verification and synthesis.     

Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java

This paper shows how to integrate two complementary techniques for manipulating program invariants: dynamic detection and static verification. Dynamic detection proposes likely invariants based on program executions, but the resulting properties are not guaranteed to be true over all possible executions. Static verification checks that properties are always true, but it can be difficult and tedious to select a goal and to annotate programs for input to a static checker. Combining these techniques overcomes the weaknesses of each: dynamically detected invariants can annotate a program or provide goals for static verification, and static verification can confirm properties proposed by a dynamic tool.We have integrated a tool for dynamically detecting likely program invariants, Daikon, with a tool for statically verifying program properties, ESC/Java. Daikon examines run-time values of program variables; it looks for patterns and relationships in those values, and it reports properties that are never falsified during test runs and that satisfy certain other conditions, such as being statistically justified. ESC/Java takes as input a Java program annotated with preconditions, postconditions, and other assertions, and it reports which annotations cannot be statically verified and also warns of potential runtime errors, such as null dereferences and out-of-bounds array indices.Our prototype system runs Daikon, inserts its output into code as ESC/Java annotations, and then runs ESC/Java, which reports unverifiable annotations. The entire process is completely automatic, though users may provide guidance in order to improve results if desired. In preliminary experiments, ESC/Java verified all or most of the invariants proposed by Daikon.