Paper Info
Title
Floats and Ropes: A Case Study for Formal Numerical Program Verification
Abstract
We present a case study of a formal verification of a numerical program that computes the discretization of a simple partial differential equation. Bounding the rounding error was tricky as the usual idea, that is to bound the absolute value of the error at each step, fails. Our idea is to find out a precise analytical expression that cancels with itself at the next step, and to formally prove the correctness of this approach.
Year
DOI
Venue
2009
10.1007/978-3-642-02930-1_8
Lecture Notes in Computer Science
Keywords
Field
DocType
simple partial differential equation,formal numerical program verification,numerical program,case study,precise analytical expression,usual idea,absolute value,next step,rounding error,formal verification,partial differential equation
Discretization,Discrete mathematics,Computer science,Round-off error,Correctness,Algorithm,Interval arithmetic,Partial differential equation,Bounding overwatch,Formal verification,Proof assistant
Conference
Volume
ISSN
Citations 
5556
0302-9743
8
PageRank 
References 
Authors
0.58
11
1
Name
Order
Citations
PageRank
Sylvie Boldo129226.85