Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Q5685720 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4222737 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certain Rational Functions Whose Power Series Have Positive Coefficients / rank
 
Normal rank
Property / cites work
 
Property / cites work: A decision procedure for linear ``big O'' equations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings. / rank
 
Normal rank
Property / cites work
 
Property / cites work: A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing / rank
 
Normal rank
Property / cites work
 
Property / cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Canonical Big Operators / rank
 
Normal rank
Property / cites work
 
Property / cites work: Floats and Ropes: A Case Study for Formal Numerical Program Verification / rank
 
Normal rank
Property / cites work
 
Property / cites work: Combining Coq and Gappa for Certifying Floating-Point Programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formal Proof of a Wave Equation Resolution Scheme: The Method Error / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4285490 / rank
 
Normal rank
Property / cites work
 
Property / cites work: CC(X): Semantic Combination of Congruence Closure with Solvable Theories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5753923 / rank
 
Normal rank
Property / cites work
 
Property / cites work: On the Partial Difference Equations of Mathematical Physics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Programming Languages and Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certification of bounds on expressions involving rounded operators / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4790659 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754041 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nonstandard analysis in ACL2 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4736391 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4231030 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Theorem Proving in Higher Order Logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: A computer-verified monadic functional implementation of the integral / rank
 
Normal rank
Property / cites work
 
Property / cites work: Type classes for efficient exact real arithmetic in Coq / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof-irrelevant model of CC with predicative induction and judgmental equality / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4435471 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4484344 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5817365 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certified Exact Transcendental Real Number Computation in Coq / rank
 
Normal rank
Property / cites work
 
Property / cites work: Propagation of round-off errors and the role of stability in numerical methods for linear and nonlinear PDEs / rank
 
Normal rank
Property / cites work
 
Property / cites work: \({\mathcal L}\)-convergence paradox in numerical methods for PDEs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4855462 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Hilbert's ‘<i>Verunglückter Beweis</i>’, the first epsilon theorem, and consistency proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4224234 / rank
 
Normal rank

Latest revision as of 15:25, 6 July 2024

scientific article
Language Label Description Also known as
English
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
scientific article

    Statements

    Wave equation numerical resolution: a comprehensive mechanized proof of a C program (English)
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    5 July 2013
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    formal proof of numerical program
    0 references
    convergence of numerical scheme
    0 references
    proof of C program
    0 references
    Coq formal proof
    0 references
    acoustic wave equation
    0 references
    partial differential equation
    0 references
    rounding error analysis
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references