{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T12:31:00Z","timestamp":1670329860014},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[1980,1]]},"DOI":"10.1145\/322169.322185","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:26:10Z","timestamp":1027769170000},"page":"191-205","source":"Crossref","is-referenced-by-count":38,"title":["Verification Decidability of Presburger Array Programs"],"prefix":"10.1145","volume":"27","author":[{"given":"Norihisa","family":"Suzuki","sequence":"first","affiliation":[{"name":"Xerox Palo Alto Research Center, 3333 Coyote Hill Road, Palo Alto, CA and Carnegie-Mellon University, Pittsburgh, Pennsylvania"}]},{"given":"David","family":"Jefferson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie-Mellon University, Schenley Park, Pittsburgh, PA"}]}],"member":"320","published-online":{"date-parts":[[1980,1]]},"reference":[{"key":"e_1_2_1_1_2","volume-title":"W Solvable Cases of the Decision Problem North-Holland","author":"ACKERMANN","year":"1954","unstructured":"ACKERMANN , W Solvable Cases of the Decision Problem North-Holland , Amsterdam , 1954 ACKERMANN, W Solvable Cases of the Decision Problem North-Holland, Amsterdam, 1954"},{"key":"e_1_2_1_2_2","volume-title":"J C Stmple programs realize exactly Presberger formulas SIAM J Comptng 5, 4 (Dec","author":"Ctte V","year":"1976","unstructured":"Ctte V , Nt AVSKX , J C Stmple programs realize exactly Presberger formulas SIAM J Comptng 5, 4 (Dec 1976 ), 666-677 CtteV, NtAVSKX, J C Stmple programs realize exactly Presberger formulas SIAM J Comptng 5, 4 (Dec 1976), 666-677"},{"key":"e_1_2_1_3_2","first-page":"57","volume-title":"Houston","author":"Erm R","year":"1976","unstructured":"DOWNEY, P.J, AND S Erm , R Assignment commands and array structures 17th Annual Syrup Foundauons Comptr Sc~ , Houston , Texas , 1976 , pp 57 - 66 . DOWNEY, P.J, AND SErm, R Assignment commands and array structures 17th Annual Syrup Foundauons Comptr Sc~, Houston, Texas, 1976, pp 57-66."},{"key":"e_1_2_1_4_2","volume-title":"P. Grundlagen der Mathemat~k, VoL 1","author":"R~r D","year":"1968","unstructured":"HILBE R~r , D , AND Bv gN^Ys , P. Grundlagen der Mathemat~k, VoL 1 . Sprmger-Verlag , Berhn , 1968 HILBER~r, D, AND Bv gN^Ys, P. Grundlagen der Mathemat~k, VoL 1. Sprmger-Verlag, Berhn, 1968"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/321439.321447"},{"key":"e_1_2_1_6_2","volume-title":"Carnegie-Mellon U, Pmsburgh, Pa","year":"1969","unstructured":"KING, J C. A program verifier Ph D th , Carnegie-Mellon U, Pmsburgh, Pa , 1969 KING, J C. A program verifier Ph D th, Carnegie-Mellon U, Pmsburgh, Pa, 1969"},{"key":"e_1_2_1_7_2","first-page":"24","volume-title":"Seminars in Mathematics. Vol 4","author":"Hn' S, V.A.","year":"1969","unstructured":"LIFS Hn' S, V.A. Some reducuon classes and undec~dable theories In Studies m Constructive Mathemattcs and Mathematical Logic , Pt L A O Shsenko, Ed., Seminars in Mathematics. Vol 4 , V A Steklov Mathematical Insmute , Leningrad , 1969 , pp 24 - 25 LIFSHn'S, V.A. Some reducuon classes and undec~dable theories In Studies m Constructive Mathemattcs and Mathematical Logic, Pt L A O Shsenko, Ed., Seminars in Mathematics. Vol 4, V A Steklov Mathematical Insmute, Leningrad, 1969, pp 24-25"},{"key":"e_1_2_1_8_2","first-page":"21","volume-title":"IFIP Congr 1962","author":"Mc CARTHY, J","year":"1962","unstructured":"Mc CARTHY, J Towards a mathematlcal science of computaUon Proc . IFIP Congr 1962 , North-Holland, Amsterdam , 1962 , pp 21 - 28 McCARTHY, J Towards a mathematlcal science of computaUon Proc. IFIP Congr 1962, North-Holland, Amsterdam, 1962, pp 21-28"},{"key":"e_1_2_1_9_2","volume-title":"Florence, Ky.","author":"MENDELSON","year":"1964","unstructured":"MENDELSON , E introductwn to Mathematical Logic Van Nostrand , Florence, Ky. , 1964 MENDELSON, E introductwn to Mathematical Logic Van Nostrand, Florence, Ky., 1964"},{"key":"e_1_2_1_10_2","volume-title":"n. A 22:` upper bound on the complexity of Presburger anthmeUc J Comptr Syst Scl 16, 3 (June","author":"OPPEN","year":"1978","unstructured":"OPPEN , n. A 22:` upper bound on the complexity of Presburger anthmeUc J Comptr Syst Scl 16, 3 (June 1978 ), 323-332 OPPEN, n. A 22:` upper bound on the complexity of Presburger anthmeUc J Comptr Syst Scl 16, 3 (June 1978), 323-332"},{"key":"e_1_2_1_11_2","volume-title":"Menlo Park, Cahf, 1977, also presented at Workshop on Automatic Deductions","year":"1977","unstructured":"SHOSTAK, R E An eff~oent decision procedure for arithmetic w~th function symbols SRI Teeh Rep CSL- 65, Stanford Research Insatute , Menlo Park, Cahf, 1977, also presented at Workshop on Automatic Deductions , Cambridge, Mass , July 1977 SHOSTAK, R E An eff~oent decision procedure for arithmetic w~th function symbols SRI Teeh Rep CSL- 65, Stanford Research Insatute, Menlo Park, Cahf, 1977, also presented at Workshop on Automatic Deductions, Cambridge, Mass, July 1977"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808471"},{"key":"e_1_2_1_13_2","volume-title":"Santa Momca","year":"1948","unstructured":"TARSKI,A A decision method for elementary algebra and geometry RAND Corp ., Santa Momca , Cahf , 1948 TARSKI,A A decision method for elementary algebra and geometry RAND Corp., Santa Momca, Cahf, 1948"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/322169.322185","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,5]],"date-time":"2022-12-05T19:50:49Z","timestamp":1670269849000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/322169.322185"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980,1]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1980,1]]}},"alternative-id":["10.1145\/322169.322185"],"URL":"http:\/\/dx.doi.org\/10.1145\/322169.322185","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[1980,1]]}}}