{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:57Z","timestamp":1742617197732,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_13","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:28:44Z","timestamp":1330298924000},"page":"237-257","source":"Crossref","is-referenced-by-count":2,"title":["Mathematical modeling and analysis of an external memory manager"],"prefix":"10.1007","author":[{"given":"William D.","family":"Young","sequence":"first","affiliation":[]},{"given":"William R.","family":"Bevier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"4","key":"13_CR1","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"W.R. Bevier, W.A. Hunt, Jr., J S. Moore, and W.D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411\u2013428, December 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR2","volume-title":"Programming under Mach.","author":"J. Boykin","year":"1993","unstructured":"J. Boykin, D. Kirschen, A. Langerman, and S. LoVerso. Programming under Mach. Addison Wesley Unix and Open Series System, Reading, Mass., 1993."},{"doi-asserted-by":"crossref","unstructured":"B. Brock, M. Kaufmann and J Strother Moore. ACL2 theorems about commercial microprocessors, in M. Srivas and A. Camilleri, eds., Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275\u2013293, 1996.","key":"13_CR3","DOI":"10.1007\/BFb0031816"},{"key":"13_CR4","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988."},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control, in D. Dill, ed., Computer Aided Verification, Lecture Notes in Computer Science 818, Springer Verlag, 1994, page 68\u201380.","key":"13_CR5","DOI":"10.1007\/3-540-58179-0_44"},{"doi-asserted-by":"crossref","unstructured":"M. Kaufmann and J Moore. An industrial strength theorem prover for a logic based on Common Lisp, to appear in IEEE Transactions on Software Engineering, 1997. This is a revised version of \u201cACL2: An industrial strength version of Nqthm,\u201d which appeared in Proceedings of the Eleventh Annual Conference on Computer Assurance, IEEE Computer Society Press, June, 1996, pp 23\u201334.","key":"13_CR6","DOI":"10.1109\/CMPASS.1996.507872"},{"unstructured":"W.D. Young and W.R. Bevier. Mathematical modeling and analysis of an external memory manager. CLI Technical Report 105, Computational Logic, Inc., September, 1995.","key":"13_CR7"}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:43:52Z","timestamp":1742600632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}