共查询到20条相似文献,搜索用时 26 毫秒
1.
2.
3.
We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper with much less guidance than existing general purpose theorem provers require for algebraic reasoning. 相似文献
4.
Deepak Kapur Mahadevan Subramaniam 《International Journal on Software Tools for Technology Transfer (STTT)》2000,3(1):32-65
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. 相似文献
5.
6.
7.
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. 相似文献
8.
9.
10.
We report on the formal verification of the floating point unit used in the VAMP processor. The dual-precision FPU is IEEE compliant and supports denormals and exceptions in hardware. The supported operations are addition, subtraction, multiplication, division, comparison, and conversions.We have formalized the IEEE standard 754. The formalization is supplemented by a rich theory of rounding, which includes notations and theorems facilitating the verification of the actual hardware. The theory of rounding enables the separation of the hardware into smaller modules which can be verified individually. Each module is verified on the gate level against a formal specification. The combination of these formal specifications, together with the theorems from the theory of rounding, yield the overall correctness of the FPU, i.e., theorems stating that the gate-level hardware complies with the high-level formalization of the IEEE standard. The verification is done completely in the theorem prover PVS.We further report on the implementation and test of the verified FPU on a Xilinx FPGA. 相似文献
11.
12.
Skeleton-based edge bundling for graph visualization 总被引:1,自引:0,他引:1
Ersoy O Hurter C Paulovich FV Cantareiro G Telea A 《IEEE transactions on visualization and computer graphics》2011,17(12):2364-2373
In this paper, we present a novel approach for constructing bundled layouts of general graphs. As layout cues for bundles, we use medial axes, or skeletons, of edges which are similar in terms of position information. We combine edge clustering, distance fields, and 2D skeletonization to construct progressively bundled layouts for general graphs by iteratively attracting edges towards the centerlines of level sets of their distance fields. Apart from clustering, our entire pipeline is image-based with an efficient implementation in graphics hardware. Besides speed and implementation simplicity, our method allows explicit control of the emphasis on structure of the bundled layout, i.e. the creation of strongly branching (organic-like) or smooth bundles. We demonstrate our method on several large real-world graphs. 相似文献
13.
《IEEE transactions on pattern analysis and machine intelligence》1987,(2):151-156
Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a specification written in SPECIAL (the specification language of HDM). In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center A1 evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process. In concept, it is open-ended. We introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality. 相似文献
14.
Paolo Traverso Piergiorgio Bertoli 《International Journal on Software Tools for Technology Transfer (STTT)》2000,3(1):78-92
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. 相似文献
15.
Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification. 相似文献
16.
Scott Uk-Jin Lee Gillian Dobbie Jing Sun Lindsay Groves 《Formal Methods in System Design》2010,37(1):1-60
The wide adoption of semistructured data has created a growing need for effective ways to ensure the correctness of its organization.
One effective way to achieve this goal is through formal specification and automated verification. This paper presents a theorem
proving approach towards verifying that a particular design or organization of semistructured data is correct. We formally
specify the semantics of the Object Relationship Attribute data model for Semistructured Data (ORA-SS) modeling notation and
its correctness criteria for semistructured data normalization using the Prototype Verification System (PVS). The result is
that effective verification on semistructured data models and their normalization can be carried out using the PVS theorem
prover. 相似文献
17.
近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明. 相似文献
18.
This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation
and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language
ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present
a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study,
we show the verification of a practical firewall system. 相似文献
19.
20.
王荣生 《计算机应用与软件》1995,12(5):36-39
本文描述了CMOS单元电路版图自动设计程序是自动电路版图设计系统的一个组成部分,它通过一列变换,将单元电器描述翻译成单元电路版图的几何描述。其特点是允许单元内多端口线网布和允许在单元四周指定端口,并对单元电路版图进行优化,因此,只要输入单元电路描述,便可自动产生单元电路的版图文件。 相似文献