{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085562},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105402","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"141-156","source":"Crossref","is-referenced-by-count":24,"title":["Elements of mathematical analysis in PVS"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Dutertre","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"10_CR1","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. In WIFT'95 Workshop on Industrial-Strength Formal Specification Techniques, April 1995."},{"key":"10_CR2","unstructured":"B. Dutertre. Coherent Requirements of the SafeFM Case Study. Technical Report SafeFM-050-RH-2, SafeFM project, September 1995."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In D. Kapur, editor, Automated Deduction\u2014CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567\u2013581. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_192"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. Imps: An Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR5","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. The Imps user's manual. Technical Report M-93B138, The Mitre Corporation, 1993."},{"key":"10_CR6","first-page":"1133","volume":"38","author":"W. M. Farmer","year":"1991","unstructured":"W. M. Farmer and F. J. Thayer. Two computer-supported proofs in metric space topology. Notices of the American Mathematical Society, 38:1133\u20131138, 1991.","journal-title":"Notices of the American Mathematical Society"},{"key":"10_CR7","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"issue":"1\/2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF01384233","volume":"4","author":"J. Harrison","year":"1994","unstructured":"J. Harrison. Constructing the real numbers in HOL. Formal Methods in System Design, 4(1\/2):35\u201359, July 1994.","journal-title":"Formal Methods in System Design"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"J. Harrison. Floating point verification in HOL. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 971 of Lecture Notes in Computer Science, pages 186\u2013199. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_65"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In J. J. Joyce and C.-J. H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications (HUG'93), volume 780 of Lecture Notes in Computer Science, pages 174\u2013184. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"J. Hooman. Correctness of Real Time Systems by Construction. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 19\u201340. Springer-Verlag, LNCS 863, September 1994.","DOI":"10.1007\/3-540-58468-4_158"},{"key":"10_CR12","unstructured":"D. Jamsek, R. W. Butler, S. Owre, and C. M. Holloway. PVS finite sets library, 1995. Part of the standard PVS distribution."},{"key":"10_CR13","unstructured":"S. Lang. Analysis I. Addison-Wesley, 1968."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"S. P. Miller and M. Srivas. Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods. In WIFT'95 Workshop on Industrial-Strength Formal Specification Techniques, April 1995.","DOI":"10.1109\/WIFT.1995.515475"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR16","unstructured":"S. Owre and N. Shankar. The Formal Semantics of PVS. Technical report, Computer Science Lab., SRI International, June 1995."},{"key":"10_CR17","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Lab., SRI International, April 1993."},{"key":"10_CR18","unstructured":"N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A reference Manual. Computer Science Lab., SRI International, March 1993."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:44:03Z","timestamp":1560937443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0105402","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}