Trusting computations: A mechanized proof from partial differential equations to actual program
- 1 August 2014
- journal article
- research article
- Published by Elsevier BV in Computers & Mathematics with Applications
- Vol. 68 (3), 325-352
- https://doi.org/10.1016/j.camwa.2014.06.004
Abstract
No abstract availableKeywords
This publication has 18 references indexed in Scilit:
- Adaptive Inexact Newton Methods with A Posteriori Stopping Criteria for Nonlinear Diffusion PDEsSIAM Journal on Scientific Computing, 2013
- seL4Communications of the ACM, 2010
- Certification of bounds on expressions involving rounded operatorsACM Transactions on Mathematical Software, 2010
- Formal verification of a realistic compilerCommunications of the ACM, 2009
- CC(X): Semantic Combination of Congruence Closure with Solvable TheoriesElectronic Notes in Theoretical Computer Science, 2008
- The method of creative telescopingJournal of Symbolic Computation, 1991
- What every computer scientist should know about floating-point arithmeticACM Computing Surveys, 1991
- A fast algorithm for proving terminating hypergeometric identitiesDiscrete Mathematics, 1990
- Positive Sums of the Classical Orthogonal PolynomialsSIAM Journal on Mathematical Analysis, 1977
- Guarded commands, nondeterminacy and formal derivation of programsCommunications of the ACM, 1975