The pitfalls of verifying floating-point computations

The pitfalls of verifying floating-point computations David Monniaux [En] This is a good article about floating point computation, especially problematic behaviour of x87. (double-rounding, extended exponent bits, etc…) Although x87’s extended precision(80bits) is a part of IEEE 754 standard, this article tells us that we must not use x87 and must use SSE2 asContinue reading “The pitfalls of verifying floating-point computations”

Enhanced Motion Blur Calculation with Optical Flow

Image from Enhanced Motion Blur Calculation with Optical Flow. [Zheng et al. 2006] Zheng, Yuanfang ; Köstler, Harald ; Thürey, Nils ; Rüde, Ulrich: Enhanced Motion Blur Calculation with Optical Flow . In: Aka GmbH (Hrsg.) : RWTH Aachen (Veranst.) : Proceedings of Vision, Modeling and Visualization 2006 (Vision, Modeling and Visualization Aachen 22. –Continue reading “Enhanced Motion Blur Calculation with Optical Flow”

Why I’m eager for realtime raytracing and MC based GI.

[En] In short, it’s simple. Because I ensures that commoditized realtime raytracing(in short term, within ~ 5 years) and commoditized Monte Carlo raytracing based Global Illumination(in long term, within ~ 20 years. After realtime rayracing era) are the most realizable destruptive innovation for realtime/offline graphics. I forecasts rasterizer based commodity HW graphics technology(such like currentContinue reading “Why I’m eager for realtime raytracing and MC based GI.”

Gappa : automatic proof generation of arithmetic properties [En] Gappa is a cool program which validates your floating-point code. Here is an example of gappa code(Cauculates x * (1-x) in [0, 1]. Taken from gappa’s site). { x in [0,1] -> float(x * float(1 – x)) in ? } Then, gappa automatically computes it’s error bound, $ echo “{ x in [0,1]Continue reading “Gappa : automatic proof generation of arithmetic properties”

Caduceus : a verification tool for C programs [En] TODO… [Ja] Haskell -> QuickCheck 自動テストツール -> Coq 証明支援ツール -> Why 検証ツール -> Caduceus C プログラム用検証ツール(Why を使う) という感じの流れで見つけたツール。 Caduceus は C 言語用の検証ツールで、たとえば [1] にあるように、 まず以下のようにソースコードにアノテーションで検証のロジックを書きます。 /*@ requires y/2 <= x <= 2*y @ ensures @ \result == x-y @*/ float Sterbenz(float x, float y) { return x-y; } すると、Caduceus は、この Sterbenz 関数の実装は、 y/2Continue reading “Caduceus : a verification tool for C programs”