{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:33Z","timestamp":1725576273633},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232124"},{"type":"electronic","value":"9783540302100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30210-0_23","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:34:36Z","timestamp":1295346876000},"page":"271-275","source":"Crossref","is-referenced-by-count":2,"title":["Abstraction-Driven Verification of Array Programs"],"prefix":"10.1007","author":[{"given":"David","family":"D\u00e9harbe","sequence":"first","affiliation":[]},{"given":"Abdessamad","family":"Imine","sequence":"additional","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Info. and Comp.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Info. and Comp."},{"key":"23_CR2","volume-title":"Proc. of the 1st Int. Conf. on Software Engineering and Formal Methods (SEFM 2003)","author":"D. D\u00e9harbe","year":"2003","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. of the 1st Int. Conf. on Software Engineering and Formal Methods (SEFM 2003), IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"23_CR3","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Lab (2003)"},{"key":"23_CR4","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Pr., London (1972)"},{"key":"23_CR5","unstructured":"Filli\u00e2tre, J.-C., Magaud, N.: Certification of Sorting Algorithms in the System Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"issue":"2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand. of Automated Reasoning (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"23_CR9","volume-title":"Handbook of Automated Reasoning, chapter Computing Small Clause Normal Forms","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Handbook of Automated Reasoning, chapter Computing Small Clause Normal Forms. Elsevier Science, Amsterdam (2001)"},{"issue":"1","key":"23_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N. Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.R.: Verification Decidability of Presburger Array Programs. J. of the ACM\u00a027(1), 191\u2013205 (1980)","journal-title":"J. of the ACM"},{"key":"23_CR11","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Front. of Combining Systems: Proc. of the 1st Int. Workshop","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Front. of Combining Systems: Proc. of the 1st Int. Workshop, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"23_CR12","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF01543480","volume":"5","author":"P. Hentenryck van","year":"1992","unstructured":"van Hentenryck, P., Graf, T.: Standard Forms for Rational Linear Arithmetics in Constraint Logic Programming. Ann. of Math. and Art. Intell.\u00a05, 303\u2013319 (1992)","journal-title":"Ann. of Math. and Art. Intell."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30210-0_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:55:58Z","timestamp":1620014158000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}