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

@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+L05
@@ Property / Mathematics Subject Classification ID: 35L05 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+M22
@@ Property / Mathematics Subject Classification ID: 65M22 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+G50
@@ Property / Mathematics Subject Classification ID: 65G50 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6184681
@@ Property / zbMATH DE Number: 6184681 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+formal proof of numerical program
@@ Property / zbMATH Keywords: formal proof of numerical program / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+convergence of numerical scheme
@@ Property / zbMATH Keywords: convergence of numerical scheme / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+proof of C program
@@ Property / zbMATH Keywords: proof of C program / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Coq formal proof
@@ Property / zbMATH Keywords: Coq formal proof / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+acoustic wave equation
@@ Property / zbMATH Keywords: acoustic wave equation / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+partial differential equation
@@ Property / zbMATH Keywords: partial differential equation / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+rounding error analysis
@@ Property / zbMATH Keywords: rounding error analysis / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KRAKATOA
@@ Property / describes a project that uses: KRAKATOA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACSL
@@ Property / describes a project that uses: ACSL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Caduceus
@@ Property / describes a project that uses: Caduceus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cvc3
@@ Property / describes a project that uses: cvc3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ASTREE
@@ Property / describes a project that uses: ASTREE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gappa
@@ Property / describes a project that uses: Gappa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flocq
@@ Property / describes a project that uses: Flocq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Why3
@@ Property / describes a project that uses: Why3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2147177731
@@ Property / OpenAlex ID: W2147177731 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.1795
@@ Property / arXiv ID: 1112.1795 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5685720
@@ Property / cites work: Q5685720 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4222737
@@ Property / cites work: Q4222737 / rank @@
+Normal rank
@@ Property / cites work @@
+Certain Rational Functions Whose Power Series Have Positive Coefficients
+Normal rank
@@ Property / cites work @@
+A decision procedure for linear ``big O'' equations
+Normal rank
@@ Property / cites work @@
+Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
+Normal rank
@@ Property / cites work @@
+A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing
+Normal rank
@@ 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.
+Normal rank
@@ Property / cites work @@
+Canonical Big Operators
@@ Property / cites work: Canonical Big Operators / rank @@
+Normal rank
@@ Property / cites work @@
+Floats and Ropes: A Case Study for Formal Numerical Program Verification
+Normal rank
@@ Property / cites work @@
+Combining Coq and Gappa for Certifying Floating-Point Programs
+Normal rank
@@ Property / cites work @@
+Formal Proof of a Wave Equation Resolution Scheme: The Method Error
+Normal rank
@@ Property / cites work @@
+Q4285490
@@ Property / cites work: Q4285490 / rank @@
+Normal rank
@@ Property / cites work @@
+CC(X): Semantic Combination of Congruence Closure with Solvable Theories
+Normal rank
@@ Property / cites work @@
+Q5753923
@@ Property / cites work: Q5753923 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Partial Difference Equations of Mathematical Physics
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of bounds on expressions involving rounded operators
+Normal rank
@@ Property / cites work @@
+Q4790659
@@ Property / cites work: Q4790659 / rank @@
+Normal rank
@@ Property / cites work @@
+Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
+Normal rank
@@ Property / cites work @@
+Q2754041
@@ Property / cites work: Q2754041 / rank @@
+Normal rank
@@ Property / cites work @@
+Nonstandard analysis in ACL2
@@ Property / cites work: Nonstandard analysis in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736391
@@ Property / cites work: Q4736391 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4231030
@@ Property / cites work: Q4231030 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+A computer-verified monadic functional implementation of the integral
+Normal rank
@@ Property / cites work @@
+Type classes for efficient exact real arithmetic in Coq
+Normal rank
@@ Property / cites work @@
+Proof-irrelevant model of CC with predicative induction and judgmental equality
+Normal rank
@@ Property / cites work @@
+Q4435471
@@ Property / cites work: Q4435471 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484344
@@ Property / cites work: Q4484344 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5817365
@@ Property / cites work: Q5817365 / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Exact Transcendental Real Number Computation in Coq
+Normal rank
@@ Property / cites work @@
+Propagation of round-off errors and the role of stability in numerical methods for linear and nonlinear PDEs
+Normal rank
@@ Property / cites work @@
+\({\mathcal L}\)-convergence paradox in numerical methods for PDEs
+Normal rank
@@ Property / cites work @@
+Q4855462
@@ Property / cites work: Q4855462 / rank @@
+Normal rank
@@ Property / cites work @@
+Hilbert's ‘<i>Verunglückter Beweis</i>’, the first epsilon theorem, and consistency proofs
+Normal rank
@@ Property / cites work @@
+Q4224234
@@ Property / cites work: Q4224234 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:352952