{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:16Z","timestamp":1725453976665},"publisher-location":"Berlin\/Heidelberg","reference-count":24,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540115587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0000050","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T06:26:23Z","timestamp":1128493583000},"page":"32-49","source":"Crossref","is-referenced-by-count":10,"title":["STP: A mechanized logic for specification and verification"],"prefix":"10.1007","author":[{"given":"R. E.","family":"Shostak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Schwartz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. M.","family":"Melliar-Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","volume-title":"Memo ATP-18","author":"W.W. Bledsoe","year":"1974","unstructured":"Bledsoe, W.W., \u201cThe Sup-inf method in Presburger arithmetic\u201d, Memo ATP-18, Mathematics Dept., Univ. of Texas, Austin, Texas, Dec. 1974."},{"key":"2_CR2","unstructured":"Boyer, R., J Moore, \u201cA computational logic\u201d, Academic Press, 1979."},{"key":"2_CR3","unstructured":"Burstall, R., J. Goguen, \u201cPutting theories together to make specifications\u201d, Proc. IJCAI, August 1977."},{"key":"2_CR4","unstructured":"Elspas, B., et al. \u201cA Jovial Verifier\u201d, SRI International, June, 1979."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Ferro, A., E. Omodeo, J. Schwartz, \u201cDecision procedures for some fragments of set theory\u201d, 5th Conf on Automated Deduction, July 1980.","DOI":"10.1007\/3-540-10009-1_8"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Good, D., R. M. Cohen, J. Keeton-Williams, \u201cPrinciples of proving concurrent programs in Gypsy\u201d, Proc 6th POPL, 1979.","DOI":"10.1145\/567752.567757"},{"key":"2_CR7","unstructured":"King, J., \u201cA program verifier\u201d, Ph.D. thesis, CMU, 1969."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Levitt, K., R. Waldinger, \u201cReasoning about programs\u201d, AI Journal 5, 1974.","DOI":"10.1016\/0004-3702(74)90015-0"},{"key":"2_CR9","unstructured":"Levitt, K., L. Robinson, B. Silverberg, \u201cThe HDM handbook\u201d, SRI International, 1979."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Luckham, D., N. Suzuki, \u201cVerification of array, record, and pointer operations in Pascal\u201d, TOPLAS, Oct, 1979.","DOI":"10.1145\/357073.357078"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Melliar-Smith, P. M., R. L. Schwartz, \u201cFormal specification and mechanical verification of SIFT: a fault-tolerant flight control system\u201d, IEEE Transactions on Computers, July 1982.","DOI":"10.1109\/TC.1982.1676059"},{"key":"2_CR12","unstructured":"Milner, R., \u201cAn algebraic definition of simulation between programs, CS 205, Stanford, 1971."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Milner, R., \u201cLCF: a way of doing proofs with a machine\u201d, Proc 8th MFCS Symp, 1979.","DOI":"10.1007\/3-540-09526-8_11"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Musser, D., \u201cAbstract data type specification in the Affirm system\u201d, IEEE TSE, Jan. 1980.","DOI":"10.1109\/TSE.1980.230459"},{"key":"2_CR15","unstructured":"Nakajima, R., M. Honda, H. Nakahara, \u201cDescribing and verifying programs with abstract data types\u201d, Formal Description of Programming Concepts, North Holland, 1977."},{"key":"2_CR16","unstructured":"Oppen, D., G. Nelson, \u201cA simplifier based on efficient decision algorithms\u201d, Proceedings of Fifth POPL, Tucson, Arizona, Jan. 1978."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Parnas, D., \u201cA technique for software module specification with examples\u201d, CACM, May 1972.","DOI":"10.1145\/355602.361309"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Robinson, L., K. Levitt, \u201cProof techniques for hierarchically structured programs\u201d, CACM, April 1977.","DOI":"10.1145\/359461.359483"},{"key":"2_CR19","unstructured":"Schorre, V., J. Stein, \u201cThe interactive theorem prover (ITP) user manual\u201d, TM-6889\/000\/01, SDC, 1980."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Shostak, R., \u201cA practical decision procedure for arithmetic with function symbols\u201d, JACM, April 1979.","DOI":"10.1145\/322123.322137"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Shostak, R., \u201cDeciding Combinations of Theories\u201d, Proceedings of the Sixth Conference on Automated Deduction, June 1982.","DOI":"10.1007\/BFb0000061"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Suzuki, N., \u201cVerifying programs by algebraic and logical reduction\u201d, Proc. Int. Conf. on Reliable Software, Los Angeles, 1975.","DOI":"10.1145\/800027.808471"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Wensley, J., et al., \u201cSIFT: Design and Analysis of a Fault-tolerant Computer for Aircraft Control\u201d, Proc IEEE, Vol. 68, No. 10, Oct. 1978.","DOI":"10.1109\/PROC.1978.11114"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Weyhrauch, R., \u201cProlegamena to a theory of mechanized formal reasoning\u201d, AI Journal, 1980.","DOI":"10.1016\/B978-0-934613-03-3.50016-7"}],"container-title":["Lecture Notes in Computer Science","6th Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000050.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T09:43:03Z","timestamp":1607334183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000050"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540115587"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0000050","relation":{},"subject":[]}}