使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法．对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题．同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间．实验结果表明,该算法是实用有效的．     

RRTP - A Replacement Rule Theorem Prover

The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.     

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies, which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.     

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到提高验证效率和保证算法程序高可信的目标,具有很好的实用价值。     

CLIN-S - A Semantically Guided First-Order Theorem Prover

CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S.     

Integrating advanced reasoning into a SAT solver

1 Introduction The SAT (Satisfiability) problem is one of the basic NP problems that have been widely researched. Many problems in EDA (Electronics Design Automation) domain such as ATPG (Automatic Test Pattern Generation), Logic Synthesis, Equivalence Checking[1] and Model Checking[2] can be reduced to the SAT problem. Typical algorithms for SAT can be classified into two categories: incomplete and complete ones. The former, including GSAT[3] and WalkSAT[4], are based on local…     

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite

This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.     

Logical Cryptanalysis as a SAT Problem

Cryptographic algorithms play a key role in computer security and the formal analysis of their robustness is of utmost importance. Yet, logic and automated reasoning tools are seldom used in the analysis of a cipher, and thus one cannot often get the desired formal assurance that the cipher is free from unwanted properties that may weaken its strength.In this paper, we claim that one can feasibly encode the low-level properties of state-of-the-art cryptographic algorithms as SAT problems and then use efficient automated theorem-proving systems and SAT-solvers for reasoning about them. We call this approach logical cryptanalysis.In this framework, for instance, finding a model for a formula encoding an algorithm is equivalent to finding a key with a cryptanalytic attack. Other important properties, such as cipher integrity or algebraic closure, can also be captured as SAT problems or as quantified boolean formulae. SAT benchmarks based on the encoding of cryptographic algorithms can be used to effectively combine features of real-world problems and randomly generated problems.Here we present a case study on the U.S. Data Encryption Standard (DES) and show how to obtain a manageable encoding of its properties.We have also tested three SAT provers, TABLEAU by Crawford and Auton, SATO by Zhang, and rel-SAT by Bayardo and Schrag, on the encoding of DES, and we discuss the reasons behind their different performance.A discussion of open problems and future research concludes the paper.     

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

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

Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver

In the requirements engineering community, consistency and completeness have been identified as important properties of system specifications. Custom algorithms to verify these properties automatically have been devised for a number of specification languages, including SCR, RSML, and Statecharts. In this paper, we provide means to automatically verify completeness and consistency of Abstract State Machine (ASM) specifications. The verification is performed using a widely available tool, a SAT solver. The use of a SAT solver removes the need for designing and fine tuning language specific verification algorithms. Furthermore, the use of a SAT solver automates the verification procedure and produces a counterexample automatically when a specification is incomplete or inconsistent. We provide an algorithm to translate ASM specifications to a SAT problem instance. The translation is illustrated using the TASM toolset in conjunction with the “production cell system” case study.     

A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers

Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designed. Another way to solve a new problem is to use a generic solver and employ parallelism to reduce the solve time. In this paper we propose a parallelization scheme for a class of SAT solvers based on the DPLL procedure. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. We parallelize Satz, one of the best generic SAT solvers, with our scheme to obtain a parallel solver called PSatz. The first experimental results on random 3-SAT problems and a set of well-known structured problems show the efficiency of PSatz. PSatz is freely available and runs on any networked workstations under Unix/Linux.     

Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem

We demonstrate the use of abstraction in aiding the construction of aninteresting and difficult example in a proof-checking system. Thisexperiment demonstrates that abstraction can make proofs easier tocomprehend and to verify mechanically. To support such proof checking, wehave developed a formal theory of abstraction and added facilities for usingabstraction to the GETFOL proof-checking system.     

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.     

A Tutorial on Stålmarck's Proof Procedure for Propositional Logic

We explain Stålmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification.     

Proving Invariants of I/O Automata with TAME

This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.     

Integrating a formal method into a software engineering process with UML and Java

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP_jassda, an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts. This research was partially supported by the DFG project ForMooS (grants OL 98/3-2 and WE 2290/5-1). C. B. Jones     

ALOGTIME and a conjecture of S.A. Cook

Usingsequential, machine-independent characterization of theparallel complexity classesAC ^k andNC ^k , we establish the following conjecture of S.A. Cook. There is a free variable equational logicALV with the property thatif f, g are function symbols forALOGTIME computable functions for which f=g is provable inALV, then there are polynomial size Frege proofs for the infinite family {|f=g| _m ⁿ :n, m} of propositional tautologies. Here, the propositional formula |f=g| _m ⁿ expresses the equality off andg on inputs of length at mostn, provided that the function values are of length at mostm. We establish a related result with constant formula-depth polynomial size Frege proofs for a systemAV related to uniformAC ⁰ functions.Part of this research supported by NSF Grant # DCR-860615. Extended abstract of this paper appeared in theIEEE Proc. of Logic in Computer Science, Philadelphia (June 1990).     

A path-conservative method for a five-equation model of two-phase flow with an HLLC-type Riemann solver

Compressible multi-phase flows are found in a variety of scientific and engineering problems. The development of accurate and efficient numerical algorithms for multi-phase flow simulations remains one of the challenging issues in computational fluid dynamics. A main difficulty of numerical methods for multi-phase flows is that the model equations cannot always be written in conservative form, though they may be hyperbolic and derived from physical conservation principles. In this work, assuming a hyperbolic model, a path-conservative method is developed to deal with the non-conservative character of the equations. The method is applied to solve the five-equation model of Saurel and Abgrall for two-phase flow. As another contribution of the work, a simplified HLLC-type approximate Riemann solver is proposed to compute the Godunov state to be incorporated into the Godunov-type path-conservative method. A second order, semi-discrete version of the method is then constructed via a MUSCL reconstruction with Runge–Kutta time stepping. Moreover, the method is then extended to the two-dimensional case by directional splitting. The method is systematically assessed via a series of test problems with exact solutions, finding satisfactory results.     

Integrating waveform lidar with hyperspectral imagery for inventory of a northern temperate forest

It has been suggested that attempts to use remote sensing to map the spatial and structural patterns of individual tree species abundances in heterogeneous forests, such as those found in northeastern North America, may benefit from the integration of hyperspectral or multi-spectral information with other active sensor data such as lidar. Towards this end, we describe the integrated and individual capabilities of waveform lidar and hyperspectral data to estimate three common forest measurements - basal area (BA), above-ground biomass (AGBM) and quadratic mean stem diameter (QMSD) - in a northern temperate mixed conifer and deciduous forest. The use of this data to discriminate distribution and abundance patterns of five common and often, dominant tree species was also explored. Waveform lidar imagery was acquired in July 2003 over the 1000 ha. Bartlett Experimental Forest (BEF) in central New Hampshire (USA) using NASA's airborne Laser Vegetation Imaging Sensor (LVIS). High spectral resolution imagery was likewise acquired in August 2003 using NASA's Airborne Visible/Infrared Imaging Spectrometer (AVIRIS). Field data (2001-2003) from over 400 US Forest Service Northern Research Station (USFS NRS) plots were used to determine actual site conditions.Results suggest that the integrated data sets of hyperspectral and waveform lidar provide improved outcomes over use of either data set alone in evaluating common forest metrics. Across all forest conditions, 8-9% more of the variation in AGBM, BA, and QMSD was explained by use of the integrated sensor data in comparison to either AVIRIS or LVIS metrics applied singly, with estimated error 5-8% lower for these variables. Notably, in an analysis using integrated data limited to unmanaged forest tracts, AGBM coefficients of determination improved by 25% or more, while corresponding error levels decreased by over 25%. When data were restricted based on the presence of individual tree species within plots, AVIRIS data alone best predicted species-specific patterns of abundance as determined by species fraction of biomass. Nonetheless, use of LVIS and AVIRIS data - in tandem - produced complementary maps of estimated abundance and structure for individual tree species, providing a promising adjunct to traditional forest inventory and conservation biology planning efforts.