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

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

Specification and Verification of Concurrent Programs Through Refinements

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.     

Mechanized result verification: an industrial application

We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done “online”, at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some verification conditions; the other is done “offline”, once for all, interactively with a general purpose prover; the offline proof shows that the verification conditions checked by the online prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the online prover. This approach is called mechanized result verification. This paper describes the project requirements and explains the motivations to formal validation by mechanized result verification, provides an overview of the formalization of the specifications for the online prover and discusses in detail some issues we have addressed in the mechanized offline proof.     

A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode

We present a rigorous mathematical proof of the correctness of the floating point square root instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. We prove a statement of its correctness that corresponds directly with the IEEE Standard. We also derive an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, we describe a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction.     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

A verification system for concurrent programs based on the Boyer-Moore prover

We describe a mechanical proof system for concurrent programs, based on a formalization of the temporal framework of Manna and Pnueli as an extension of the computational logic of Boyer and Moore. The system provides a natural representation of specifications of concurrent programs as temporal logic formulas, which are automatically translated into terms that are subject to verification by the Boyer-Moore prover. Several specialized derived rules of inference are introduced to the prover in order to facilitate the verification of invariance (safety) and eventuality (liveness) properties. The utility of the system is illustrated by a correctness proof for a two-process program that computes binomial coefficients.     

基于属性访问策略的批量零知识身份认证方案

隐私保护技术主要有属性基加密、同态加密、多方安全计算等,针对属性基加密的访问控制中双线性映射耗时问题、同态加密难以非公开地验证明文计算的结果问题以及多方安全计算需要可信第三方等问题,提出了一种基于属性访问策略的批量零知识身份认证方案。该方案是基于Aurora 协议提出的,具有良好的抗量子攻击计算潜力;所提方案引入合成证明者,其作用是将各个用户生成的证明合成一个证明以减轻证明者和验证者计算开销,且设计了找出未通过认证用户的查找算法。最后对所提方案进行了安全分析、可行性分析并与其他方案进行了对比分析。经过分析该方案中验证者的时间可维持在O（n）。     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

基于二值化密集卷积神经网络的表情识别算法

人脸表情识别已成为人工智能领域的重要研究课题,但传统的卷积神经网络需要庞大的计算资源使得其应用受限,而二值化卷积神经网络可通过快速与或运算代替原本的浮点乘法运算,大大降低了算法对计算资源的需求。论文提出了一种基于数据增强和二值化卷积神经网络的人脸表情识别算法,通过均值估计,在FER2013数据集上达到了66.15%的识别率,超越了部分基于浮点乘积运算的卷积网络,为表情识别算法移植到小型设备中提供了可能。     

Floating point arithmetic teaching for computational science

Computational science is based upon numerical computing and, consequently, requires excellent knowledge of floating point computer arithmetic. In general, the average computational science student has a relatively limited understanding of the implications of floating point computation. This paper presents an initiative to teach floating point number representation and arithmetic in undergraduate courses in computational science. The approach is based on carefully designed practical exercises which highlight the main properties and computational issues of finite length number representation and arithmetic. In conjunction to the exercises, an auxiliary educational tool constitutes a valuable support for students to learn and understand the concepts involved. Simpler formats are used as an introduction to the IEEE 754 standard, with the aim of presenting the fundamentals of the floating point computation and emphasizing its limitations. This approach could be included in courses related to computer organization, programming, discrete mathematics, numerical methods or scientific computing in computational science curricula.     

Using an induction prover for verifying arithmetic circuits

We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

Mechanizing some advanced refinement concepts

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.     

Fixed point implementation of fast Kalman predictors

In this note we study scaling rules and roundoff noise variances in a fixed-point implementation of the Kalman predictor for an ARMA time series observed noise free. The Kalman predictor is realized in a fast form that uses the so-called fast Kalman gain algorithm. The algorithm for the gain is fixed point. Scaling rules and expressions for rounding error variances are derived. The numerical results show that the fixed-point realization performs very close to the floating point realization for relatively low-order ARMA time series that are not too narrow band. The predictor has been implemented in 16-bit fixed-point arithmetic on an INTEL 8086 microprocessor, and in 16-bit floating-point arithmetic on an INTEL 8080. Fixed-point code was written in Assembly language and floating-point code was written in Fortran. Experimental results were obtained by running the fixed- and floating-point filters on identical data sets. All experiments were carried out on an INTEL MIDS 230 development system.     

Mathematical Induction in Otter-Lambda

Otter-lambda is Otter modified by adding code to implement an algorithm for lambda unification. Otter is a resolution-based, clause-language first-order prover that accumulates deduced clauses and uses strategies to control the deduction and retention of clauses. This is the first time that such a first-order prover has been combined in one program with a unification algorithm capable of instantiating variables to lambda terms to assist in the deductions. The resulting prover has all the advantages of the proof-search algorithm of Otter (speed, variety of inference rules, excellent handling of equality) and also the power of lambda unification. We illustrate how these capabilities work well together by using Otter-lambda to find proofs by mathematical induction. Lambda unification instantiates the induction schema to find a useful instance of induction, and then Otter's first-order reasoning can be used to carry out the base case and induction step. If necessary, induction can be used for those, too. We present and discuss a variety of examples of inductive proofs found by Otter-lambda: some in pure Peano arithmetic, some in Peano arithmetic with defined predicates, some in theories combining algebra and the natural numbers, some involving algebraic simplification (used in the induction step) by simplification code from MathXpert, and some involving list induction instead of numerical induction. These examples demonstrate the feasibility and usefulness of adding lambda unification to a first-order prover. Research supported by NSF grant number CCR-0204362.     

Design and analysis of evolutionary bit-length optimization algorithms for floating to fixed-point conversion

Hardware designs need to obey constraints of resource utilization, minimum clock frequency, power consumption, computation precision and data range, which are all affected by the data type representation. Floating and fixed-point representations are the most common data types to work with real numbers where arithmetic hardware units for fixed-point format can improve performance and reduce energy consumption when compared to floating point solution. However, the right bit-lengths estimation for fixed-point is a time-consuming task since it is a combinatorial optimization problem of minimizing the accumulative arithmetic computation error. This work proposes two evolutionary approaches to accelerate the process of converting algorithms from floating to fixed-point format. The first is based on a classic evolutionary algorithm and the second one introduces a compact genetic algorithm, with theoretical evidence that a near-optimal performance, to find a solution, has been reached. To validate the proposed approaches, they are applied to three computing intensive algorithms from the mobile robotic scenario, where data error accumulated during execution is influenced by sensor noise and navigation environment characteristics. The proposed compact genetic algorithm accelerates the conversion process up to 10.2× against the state of art methods reaching similar bit precision and robustness.     

Formal Verification of C Systems Code

Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this paper we present a study in the mechanisation of two proof abstractions for pointer program verification in the Isabelle/HOL theorem prover, based on a low-level memory model for C. The language’s type system presents challenges for the multiple independent typed heaps (Burstall-Bornat) and separation logic proof techniques. In addition to issues arising from explicit value size/alignment, padding, type-unsafe casts and pointer address arithmetic, structured types such as C’s arrays and structs are problematic due to the non-monotonic nature of pointer and lvalue validity in the presence of the unary &-operator. For example, type-safe updates through pointers to fields of a struct break the independence of updates across typed heaps or ∧^*-conjuncts. We provide models and rules that are able to cope with these language features and types, eschewing common over-simplifications and utilising expressive shallow embeddings in higher-order logic. Two case studies are provided that demonstrate the applicability of the mechanised models to real-world systems code; a working of the standard in-place list reversal example and an overview of the verification of the L4 microkernel’s memory allocator.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure against alternative interpolation methods, both for QFPA and linear rational arithmetic.