一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

一个出具证明编译器后端的设计与实现

设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性别名问题。后端包括独立的定理检查器,能够检验携证明代码的完整性。     

自动定理证明：十年回顾

本文主要介绍近十年来定理证明器的发展情况,同时讨论了与自动定理证明相关的一些问题。     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

支持用户自定义谓词的自动定理证明的研究

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.     

一种汇编语言指针逻辑的设计与实现

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证.     

基于高阶逻辑的定理证明方法及其对策的应用

定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。     

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

关于归纳证明的探讨

归纳定理证明是一种难度较大且较有前途的一种自动定理证明方法。较早的归纳定理证明器是Boyer一Moore于1979年提出的BM证明器,BM证明器采用的是传统的结构归纳法,对所证公式中的每个函数项都根据其所谓归纳模板提出相应的归纳方案,然后对这个归纳方案进行分析、比较和整理,得出整个     

基于向量的几何可读自动证明

几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.     

A new approach to pointer analysis for assignments

Pointer analysis is a technique to identify at copile-time the potential values of the pointer expressions in a program,which promises significant benefits for optimzing and parallelizing complilers.In this paper,a new approach to pointer analysis for assignments is presented.In this approach,assignments are classified into three categories:pointer assignments,structure(union)assignents and normal assignments which don‘t affect the point-to information.Pointer analyses for these three kinds of assignments respectively make up the integrated algorithm.When analyzing a pointer assigemtn.a new method called expression expansion is used to calculate both the left targets and the right targets.The integration of recursive data structure analysis into pointer analysis is a significant originality of this paper,which uniforms the pointer analysis for heap variables and the pointer analysis for stack variables.This algorithm is implemented in Agassiz,an analyzing tool for C programs developed by Institute of Parallel Processing,Fudan University,Its accuracy and effectiveness are illustrated by experimental data.     

数据结构中链表的插入和删除方法研究

链表是数据结构中的重要概念,利用指针处理链表是教学中的一个难点。为此,对链表的插入、删除方法进行了的分析,找出了问题的关键,总结了操作过程中的实现方法和技巧,以帮助学生学习和理解该部分知识。     

An APL approach to the representation and manipulation of data structures

One of the important characteristics of a programming language is the manner in which commonly used data structures can be represented and manipulated. Methods for the representation of complex data structures in APL, a programming language based on rectangular arrays and a multiplicity of functions, are presented in this paper. Data structures considered are: strings and sets, stacks and queues, tables, linked lists, and sort trees. The material provides insight into the nature of data structures and should aid in establishing future requirements for primal and base languages.     

Towards the Validation of Plagiarism Detection Tools by Means of Grammar Evolution

Student plagiarism is a major problem in universities worldwide. In this paper, we focus on plagiarism in answers to computer programming assignments, where students mix and/or modify one or more original solutions to obtain counterfeits. Although several software tools have been developed to help the tedious and time consuming task of detecting plagiarism, little has been done to assess their quality, because determining the real authorship of the whole submission corpus is practically impossible for markers. In this paper, we present a Grammar Evolution technique which generates benchmarks for testing plagiarism detection tools. Given a programming language, our technique generates a set of original solutions to an assignment, together with a set of plagiarisms of the former set which mimic the basic plagiarism techniques performed by students. The authorship of the submission corpus is predefined by the user, providing a base for the assessment and further comparison of copy-catching tools. We give empirical evidence of the suitability of our approach by studying the behavior of one advanced plagiarism detection tool (AC) on four benchmarks coded in APL2, generated with our technique.      

The solution of linear,constant-coefficient,ordinary differential equations with APL

The matrix exponential technique is a method for solving linear, simultaneous constant-coefficient, differential equations. The method does not require matrix inversions, but rather the summing of a truncated exponential series. The matrix form of this method makes it particularly well-suited to the matrix-handling methods of APL. The essential portion of the APL program contains only fourteen APL statements; thus it can be readily programmed. The combination of matrix exponential method and the APL language provides a fast and accurate interactive means for solving this class of ordinary differential equations.     

Does APL really need run-time parsing?

Most APL systems delay all parsing until run-time. Because the APL expression language is inherently ambiguous and because identifier binding is delayed until run-time, some runtime parsing is shown to be necessary. Nevertheless we argue that most APL statement parsing can be done at entry-time and that there are several reasons for doing so. Then a technique is described whereby APL statements are partially parsed at entry-time and are parse completed at run-time.     

Harvesting relational tables from lists on the web

A large number of web pages contain data structured in the form of ??lists??. Many such lists can be further split into multi-column tables, which can then be used in more semantically meaningful tasks. However, harvesting relational tables from such lists can be a challenging task. The lists are manually generated and hence need not have well-defined templates??they have inconsistent delimiters (if any) and often have missing information. We propose a novel technique for extracting tables from lists. The technique is domain independent and operates in a fully unsupervised manner. We first use multiple sources of information to split individual lines into multiple fields and then, compare the splits across multiple lines to identify and fix incorrect splits and bad alignments. In particular, we exploit a corpus of HTML tables, also extracted from the web, to identify likely fields and good alignments. For each extracted table, we compute an extraction score that reflects our confidence in the table??s quality. We conducted an extensive experimental study using both real web lists and lists derived from tables on the web. The experiments demonstrate the ability of our technique to extract tables with high accuracy. In addition, we applied our technique on a large sample of about 100,000 lists crawled from the web. The analysis of the extracted tables has led us to believe that there are likely to be tens of millions of useful and query-able relational tables extractable from lists on the web.     

Does APL really need run-time checking?

APL in its present interpretive implementations provides an ideal tool for the development of programs. The interpretive overhead, however, often prohibits the running of large production programs. Our results indicate that the overhead involved in checking type and size compatibility of the arguments of APL primitive functions during execution can be substantially avoided without loss of error detection. Using a large sample of syntactically correct APL programs, a statistical analysis was performed on the required conformability checks for each function. We have compiled (for each type of conformability check in each program) statistics on the percentage of checks that could be eliminated by static analysis and verification. The programs analysed contained 1,454 primitive functions. Of the 2,412 rank, length, domain and value checks required by a ‘naïve’ interpreter, 1,966 (80 per cent) can be validated statically. Index checks were required only thirty-one times, but essentially all must be evaluated at run time. This suggests that compilation of APL programs to conventional target codes may be feasible as a high performance implementation whenever the cost of such translation does not dominate.     

An APL procedure to estimate genotype by environment interaction when two environments are considered

Genotype by environment interaction (GEI) is a relevant topic in many fields of applied biology. Normal parametric approaches following analysis of variance are not suitable when large differences between error variances within environments are present. We illustrate an APL program following Yamada's approach to estimate GEIs and ancillary statistics when two environments are considered. The choice of APL environment is based on its value as a useful tool in algorithm implementation and problem-solving. Its use is suggested in biological applications where matrix algebra is involved and an understanding of the computing complexity of problems is generally not required.