{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:43Z","timestamp":1725456223814},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012862","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"622-642","source":"Crossref","is-referenced-by-count":0,"title":["Two automated methods in implementation proofs"],"prefix":"10.1007","author":[{"given":"Leo","family":"Marcus","sequence":"first","affiliation":[]},{"given":"Timothy","family":"Redmond","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"43_CR1","unstructured":"Barbacci, M. R., Barnes, G.E., Cattell, R. G., and Sieiworek, D.P., \u201cThe ISPS Computer Description Language\u201d, Tech. report CMU-CS-79-137, Carnegie-Mellon University, Computer Science Department, August 1979"},{"key":"43_CR2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1109\/TSE.1976.233535","volume":"2","author":"A. Birman","year":"1976","unstructured":"Birman, A. and Joyner, W. H., \u201cA Problem-Reduction Approach to Proving Simulation Between Programs\u201d, IEEE Transactions on Software Engineering, 2 (1976) 87\u201396","journal-title":"IEEE Transactions on Software Engineering"},{"key":"43_CR3","unstructured":"Cook, J. V., \u201cFinal Report for the C\/30 Microcode Verification Project\u201d, Tech Report ATR-86(6771)-3, The Aerospace Corporation, 1986"},{"key":"43_CR4","unstructured":"Cook, J. V., \u201cC\/30 Proof\u201d, Tech. report ATR-86(6771)-4, The Aerospace Corporation, 1986."},{"key":"43_CR5","volume-title":"State Deltas: A Formalism for Representing Segments of Computation","author":"S. D. Crocker","year":"1977","unstructured":"Crocker, S. D., \u201cState Deltas: A Formalism for Representing Segments of Computation, PhD Thesis, University of California, Los Angeles, 1977."},{"key":"43_CR6","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/MS.1986.233752","volume":"3","author":"W. Damm","year":"1986","unstructured":"Damm, W., Doehmen, G., Merkel, K., and Sichelschmidt, M., \u201cThe AADL\/S* Approach to Firmware Design Verification\u201d, IEEE Software, 3 (1986) 27\u201337","journal-title":"IEEE Software"},{"key":"43_CR7","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1109\/MS.1986.234068","volume":"3","author":"S. Dasgupta","year":"1986","unstructured":"Dasgupta, S., Wilsey, P., and Heinanen, J., \u201cAxiomatic Specifications in Firmware Development Systems\u201d, IEEE Software, 3 (1986) 49\u201358","journal-title":"IEEE Software"},{"key":"43_CR8","series-title":"Tech Report","volume-title":"Report on Gypsy 2.05","author":"D. Good","year":"1986","unstructured":"Good, D., Akers, R., Smith, L. \u201cReport on Gypsy 2.05\u201d, Tech Report ICSCACMP-48, Institute for Computing Science, University of Texas, Austin, February, 1986"},{"key":"43_CR9","unstructured":"Marcus, L., \u201cSDVS 6 Users' Manual\u201d, Tech Report ATR-86A(2778)-4, The Aerospace Corporation, 1987"},{"key":"43_CR10","unstructured":"Marcus, L., Redmond, T., and Shelah, S.\u201cCompleteness of State Deltas\u201d, Tech Report ATR-85(8354)-5, The Aerospace Corporation, 1985"},{"key":"43_CR11","unstructured":"Redmond, T., \u201cComposition of State Changes and Program Verification\u201d, Tech Report ATR-86A(2778)-3, The Aerospace Corporation, 1987"},{"key":"43_CR12","unstructured":"Redmond, T. and Marcus, L, \u201cMapping between Levels and Proofs of Implementation\u201d, Tech Report ATR-86A(8554)-5, The Aerospace Corporation, 1987"},{"key":"43_CR13","unstructured":"Scheid, J., Martin, R., Anderson, S., and Holtsberg, S., \u201cINA-JO Specification Language Reference Manual, Release 1\u201d TM 6021\/001\/02, System Development Corporation, January 1986"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012862.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:43Z","timestamp":1607353603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0012862","relation":{},"subject":[]}}