Pages that link to "Item:Q352952"

The following pages link to Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952):

Displaying 18 items.

• A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms (Q1722642) (← links)
• The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
• Formal analysis of the compact position reporting algorithm (Q1996426) (← links)
• Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
• A formally verified floating-point implementation of the compact position reporting algorithm (Q2024357) (← links)
• Computer-assisted verification of four interval arithmetic operators (Q2175842) (← links)
• A two-phase approach for conditional floating-point verification (Q2233493) (← links)
• Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
• Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
• A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms (Q2829257) (← links)
• Affine Arithmetic and Applications to Real-Number Proving (Q2945641) (← links)
• Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
• Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (Q5206960) (← links)
• Quantitative continuity and Computable Analysis in Coq (Q5875440) (← links)
• Formally-verified round-off error analysis of Runge-Kutta methods (Q6149594) (← links)
• Rounding error analysis of linear recurrences using generating series (Q6163326) (← links)