检索结果-内蒙古大学图书馆

20th International Conference on Software Engineering and Formal Methods (SEFM)

作者： Rasheed, Junaid Konecny, Michal Aston Univ Birmingham B4 7ET W Midlands England

ISBN: (纸本)9783031171086;9783031171079

We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying SPARK programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps.

关键词： floating-point computation Software verification Automated proving Interval methods Software assurance

来源：评论

学校读者我要写书评

暂无评论

Verifying floating-point programs with constraint programming and abstract interpretation techniques

引用

AUTOMATED SOFTWARE ENGINEERING 2016年第2期23卷 191-217页

作者： Ponsini, Olivier Michel, Claude Rueher, Michel Univ Nice Sophia Antipolis CNRS I3S F-06900 Sophia Antipolis France

Static value analysis is a classical approach for verifying programs with floating-point computations. Value analysis mainly relies on abstract interpretation and over-approximates the possible values of program variables. State-of-the-art tools may however compute over-approximations that can be rather coarse for some very usual program expressions. In this paper, we show that constraint solvers can significantly refine approximations computed with abstract interpretation tools. More precisely, we introduce a hybrid approach combining abstract interpretation and constraint programming techniques in a single static and automatic analysis. This hybrid approach benefits from the strong points of abstract interpretation and constraint programming techniques, and thus, it is more effective than static analysers and constraint solvers, when used separately. We compared the efficiency of the system we developed-named rAiCp-with state-of-the-art static analyzers: rAiCp produces substantially more precise approximations and is able to check program properties on both academic and industrial benchmarks.

关键词： Program verification floating-point computation Constraint solving over floating-point numbers Constraint solving over real number intervals Abstract interpretation-based approximation

来源：评论

学校读者我要写书评

暂无评论

Design of an Intelligent DMA System Architecture with Data Pre-processing

Design of an Intelligent DMA System Architecture with Data P...

引用

2016 2nd International Conference on Advances in Mechanical Engineering and Industrial Informatics(AMEII 2016)

作者： Pengyi Wu Zhaolin Li Institute of Microelectronics Tsinghua University Research Institute of Information Technology Tsinghua University

ISBN: (纸本)9781510823808

DMA is often used to transfer data between different kinds of memory-mapped slave *** is a common peripheral component for *** order to make full use of the time during the reading and writing,this paper proposed an intelligent *** with the traditional DMA,a newly designed operational unit is added to the RAM-based architecture and the parameter RAM(PRAM) is improved to suits the whole DMA *** supports floating-point computation and the interface is designed based on the AMBA bus protocol *** algorithm has been used to evaluate the proposed design.

关键词： DSP DMA PRAM floating-point computation Pre-computation

来源：评论

学校读者我要写书评

暂无评论

Reproducible Tall-Skinny QR 22

Reproducible Tall-Skinny QR

引用

IEEE 22nd Symposium on Computer Arithmetic ARITH 22

作者： Demmel, James Hong Diep Nguyen Univ Calif Berkeley Berkeley CA 94720 USA

ISBN: (纸本)9781479986637

Reproducibility is the ability to obtain bitwise identical results from different runs of the same program on the same input data, regardless of the available computing resources, or how they are scheduled. Recently, techniques have been proposed to attain reproducibility for BLAS operations [1], [2], [5], all of which rely on reproducibly computing the floating-point sum and dot product. Nonetheless, a reproducible BLAS library does not automatically translate into a reproducible higher-level linear algebra library, especially when communication is optimized. For instance, for the QR factorization, conventional algorithms such as Householder transformation or Gram-Schmidt process can be used to reproducibly factorize a floating-point matrix by fixing the high-level order of computation, for example column-by-column from left to right, and by using reproducible versions of level-1 BLAS operations such as dot product and 2-norm. In a massively parallel environment, those algorithms have high communication cost due to the need for synchronization after each step. The Tall-Skinny QR algorithm obtains much better performance in massively parallel environments by reducing the number of messages by a factor of n to O(log(P)) where P is the processor count, by reducing the number of reduction operations to O(1). Those reduction operations however are highly dependent on the network topology, in particular the number of computing nodes, and therefore are difficult to implement reproducibly and with reasonable performance. In this paper we present a new technique to reproducibly compute a QR factorization for a tall skinny matrix, which is based on the Cholesky QR algorithm to attain reproducibility as well as to improve communication cost, and the iterative refinement technique to guarantee the accuracy of the computed results. Our technique exhibits strong scalability in massively parallel environments, and at the same time can provide results of almost the same accuracy a

关键词： floating-point computation Linear Algebra Reproducibility

来源：评论

学校读者我要写书评

暂无评论

A general approach to the analysis of controlled perturbation algorithms

引用

computationAL GEOMETRY-THEORY AND APPLICATIONS 2011年第9期44卷 507-528页

作者： Mehlhorn, Kurt Osbild, Ralf Sagraloff, Michael Max Planck Inst Informat D-66123 Saarbrucken Germany

Controlled Perturbation (CP, for short) is an approach to obtaining efficient and robust implementations of a large class of geometric algorithms using the computational speed of multiple precision floating point arithmetic (compared to exact arithmetic), while bypassing the precision problems by perturbation. It also allows algorithms to be written without consideration of degenerate cases. CP replaces the input objects by a set of randomly perturbed (moved, scaled, stretched, etc.) objects and protects the evaluation of geometric predicates by guards. The execution is aborted if a guard indicates that the evaluation of a predicate with floating point arithmetic may return an incorrect result. If the execution is aborted, the algorithm is rerun on a new perturbation and maybe with a higher precision of the floating point arithmetic. If the algorithm runs to completion, it returns the correct output for the perturbed input. The analysis of CP algorithms relates various parameters: the perturbation amount, the arithmetic precision, the range of input values, and the number of input objects. We present a general methodology for analyzing CP algorithms. It is powerful enough to analyze all geometric predicates that are formulated as signs of polynomials. (C) 2011 Elsevier B.V. All rights reserved.

关键词： Reliable geometric computing Controlled perturbation floating-point computation Numerical robustness problems

来源：评论

学校读者我要写书评

暂无评论

Reducing Exact computations to Obtain Exact Results Based on Stabilization Techniques

Reducing Exact Computations to Obtain Exact Results Based on...

引用

International Workshop on Symbolic-Numeric computation

作者： Shirayanagi, Kiyoshi Sekigawa, Hiroshi Tokai Univ Sch Sci Hiratsuka Kanagawa 2591292 Japan

ISBN: (纸本)9781605586649

For a certain class of algebraic algorithms, we propose a new method that reduces the number of exact computational steps needed for obtaining exact results. This method is the floating-point interval method using zero rewriting and symbols. Zero rewriting, which is from stabilization techniques, rewrites an interval coefficient into the zero interval if the interval contains zero. Symbols are used to keep track of the execution path of the original algorithm with exact computations, so that the associated real coefficients can be computed by evaluating the symbols. The key point is that at each stage of zero rewriting, one checks to see if the zero rewriting is really correct;namely, an interval that has been rewritten into zero is really zero by exploiting the associated symbol. This method mostly uses floating-point computations;the exact computations are only performed at the stage of zero rewriting and in the final evaluation to get the exact coefficients. Moreover, one does not need to check the correctness of the output.

关键词： stabilization techniques floating-point computation interval axithmetic zero rewriting exact results log

来源：评论

学校读者我要写书评

暂无评论

Computer arithmetic and sensitivity of natural measure

引用

JOURNAL OF DIFFERENCE EQUATIONS AND APPLICATIONS 2005年第7期11卷 669-676页

作者： Sauer, T George Mason Univ Dept Math Sci Fairfax VA 22030 USA

In computer simulations of deterministic dynamical systems, floating-point rounding errors and other truncation errors contaminate the simulation results. We investigate the effect of computations using IEEE standard ... 详细信息

关键词： natural measure chaotic attractor floating-point computation trajectories

来源：评论

学校读者我要写书评

暂无评论

mAgic-FPU and MADE: A customizable VLIW core and the modular VLIW processor architecture description environment

引用

COMPUTER PHYSICS COMMUNICATIONS 2001年第1期139卷 132-143页

作者： Paolucci, PS Kajfasz, P Bonnot, P Candaele, B Maufroid, D Pastoreli, E Ricciardi, A Fusella, Y Guarino, E IPITEC Srl I-00155 Rome Italy Univ Roma La Sapienza Dipartimento Fis INFN Roma I-00185 Rome Italy Thomson CSF Commun F-92231 Gennevilliers France ATMEL F-13106 Rousset France IRIS Srl I-00034 Colleferro Italy

mAgic-FPU is the architecture of a family of VLIW cores for configurable system level integration of floating and fixed point computing power. mAgic customization permits the designer to tune basic parameters, such as the computing power/memory access ratio of the core processor, the number of available arithmetic operation per cycle, the register file size and number of port, as well as of the number of arithmetic operators. The reconfiguration. (e.g., of register file size and number of port, as well as of the number of arithmetic operators) is supported by the software environment MADE (Modular VLIW processor Architecture and Assembler Description Environment). MADE reads an architecture description file and produces a customized assembler-scheduler for the target VLIW architecture, configuring a general purpose VLIW optimizer-scheduler engine. The mAgic-FPU core architecture satisfies the requisite of portability among silicon foundries. The first members of the mAgic FPU core family architecture fit the requirements of 'Smart Antenna for Adaptive Beam-Forming processing' and 'Physical Sound Synthesis'. The first 1 GigaFlops mAgic core will run at 100 MHz within an area of 40 mm(2) in 0.25 mum ATMEL CMOS technology in first half 2002. (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： VLIW architectures configurable cores floating-point computation instruction level parallelism architectural description languages embedded processing

来源：评论

学校读者我要写书评

暂无评论

Remark on ''Fast floating-point processing in Common Lisp''

引用

ACM TRANSACTIONS ON MATHEMATICAL SOFTWARE 1996年第4期22卷 496-497页

作者： Reid, JK Rutherford Appleton Lab. Oxon UK

We explain why we feel that the comparison between Common Lisp and Fortran in a recent article by Fateman et al. in this journal is not entirely fair.

关键词： Common Lisp floating-point computation Fortran Fortran 90

来源：评论

学校读者我要写书评

暂无评论

A HARDWARE-ORIENTED ALGORITHM FOR floating-point FUNCTION GENERATION

引用

IEEE TRANSACTIONS ON COMPUTERS 1991年第2期40卷 237-241页

作者： OGRADY, EP YOUNG, BK Dept. of Comput. Sci. & Eng. Arizona State Univ. Tempe AZ USA

An algorithm is presented for performing accurate, high-speed, floating point function generation for univariate functions defined at arbitrary breakpoints. Rapid identification of the breakpoint interval which includes the input argument is the key operation in the algorithm. A hardware implementation which makes extensive use of read/write memories illustrates the algorithm.

关键词： floating-point computation FUNCTION GENERATION SIMULATION TABLE LOOKUP

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：