DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Ziegler, Martin | - |
dc.contributor.advisor | 지글러, 마틴 | - |
dc.contributor.author | Park, Se Won | - |
dc.date.accessioned | 2018-06-20T06:24:15Z | - |
dc.date.available | 2018-06-20T06:24:15Z | - |
dc.date.issued | 2017 | - |
dc.identifier.uri | http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=718720&flag=dissertation | en_US |
dc.identifier.uri | http://hdl.handle.net/10203/243446 | - |
dc.description | 학위논문(석사) - 한국과학기술원 : 전산학부, 2017.8,[iii, 41 p. :] | - |
dc.description.abstract | Computing with infinite data such as real numbers cannot be performed exactly on a Turing machine. Instead, real numbers are treated as an infinite sequence of approximations. Computing a real function means that a Turing machine converts approximations to the argument into approximations of the value, according to Computable Analysis. [Brattka&Hertling’98] have suggested an equivalent but more practical model of computation over the reals: the feasible real-RAM. Based on this fundamental idea, the iRRAM library for C++ has been developed as an imperative programming language which supports abstract datatypes with exact and multivalued semantics. In this dissertation, we extend Floyd-Hoare logic to formally verify correctness of such algorithms. A set of inference rules is suggested as a systematic framework for program verification. We also consider the diagonalization of complex self--adjoint matrices with a particular emphasis on the degenerate cases, which in general are ill-posed and in fact provably uncomputable. Employing a Recursive Analysis, we have designed, implemented and evaluated several reliable algorithms on iRRAM which can compute some orthonormal basis of eigenvectors, in the sense of output approximation, up to any desired precision - provided that, in addition to approximations to the d(d+1)/2 matrix' entries, its number of distinct eigenvalues k is known/provided. | - |
dc.language | eng | - |
dc.publisher | 한국과학기술원 | - |
dc.subject | Computable Analysis▼aExact Real Computation▼aFormal Verification▼aMatrix Diagonalization | - |
dc.subject | 계산 해석학▼a실수 연산▼a프로그램 검증▼a행렬 대각화 | - |
dc.title | Verified real computation | - |
dc.title.alternative | 검증된 실수 연산 | - |
dc.type | Thesis(Master) | - |
dc.identifier.CNRN | 325007 | - |
dc.description.department | 한국과학기술원 :전산학부, | - |
dc.contributor.alternativeauthor | 박세원 | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.