{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:25:12Z","timestamp":1725549912179},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540290513"},{"type":"electronic","value":"9783540317302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11559306_4","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T12:50:36Z","timestamp":1127825436000},"page":"65-80","source":"Crossref","is-referenced-by-count":15,"title":["On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria Paola","family":"Bonacina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-30482-1_32","volume-title":"Formal Methods and Software Engineering","author":"K. Arkoudas","year":"2004","unstructured":"Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a File System Implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004, vol.\u00a03308, pp. 373\u2013390. Springer, Heidelberg (2004)"},{"key":"4_CR2","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Rusinowitch, M., Sehgal, A.K.: High-Performance Deduction for Verification: a Case Study in the Theory of Arrays. In: Notes of the 2nd VERIFY Workshop, 3rd FLoC, number 07\/2002 in Technical Reports, pp. 103\u2013112. DIKU, U. Copenhagen (2002)"},{"key":"4_CR3","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: Big Proof Engines as Little Proof Engines: New Results on Rewrite-Based Satisfiability Procedures. In: Notes of the 3rd PDPAR Workshop, CAV-17, Technical Reports. U. Edinburgh (2005)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a Rewriting Approach to Satisfiability Procedures: Theories of Data Structures, Combination Framework and Experimental Appraisal. Technical Report 36\/2005, Dip. di Informatica, U. Verona (May 2005), http:\/\/www.sci.univr.it\/~bonacina\/verify.html","DOI":"10.1007\/11559306_4"},{"issue":"2","key":"4_CR5","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. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC\u00a0Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-45988-X_11","volume-title":"Frontiers of Combining Systems","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A Generalization of Shostak\u2019s Method for Combining Decision Procedures. In: Armando, A. (ed.) FroCos 2002. LNCS, vol.\u00a02309, p. 132. Springer, Heidelberg (2002)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002, vol.\u00a02404, p. 78. Springer, Heidelberg (2002)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-25984-8_14","volume-title":"Automated Reasoning","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N.: The ICS Decision Procedures for Embedded Deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol.\u00a03097, pp. 218\u2013222. Springer, Heidelberg (2004)"},{"key":"4_CR10","volume-title":"Proc. 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. SEFM 2003. IEEE, Los Alamitos (2003)"},{"key":"4_CR11","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. Technical Report 148, HP Labs (2003)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak Light. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 332\u2013347. Springer, Heidelberg (2002)"},{"key":"4_CR13","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":"4_CR14","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":"4_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, vol.\u00a01. Elsevier Science, Amsterdam (2001)"},{"key":"4_CR16","volume-title":"Proc. LICS-16","author":"H. Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proc. LICS-16. IEEE, Los Alamitos (2001)"},{"issue":"2\u20133","key":"4_CR17","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. J. of AI Comm.\u00a015(2\u20133), 111\u2013126 (2002)","journal-title":"J. of AI Comm."},{"key":"4_CR18","unstructured":"Schulz, S., Bonacina, M.P.: On Handling Distinct Objects in the Superposition Calculus. In: Notes of the 5th Int. Workshop on Implementation of Logics, LPAR-11, March 2005, pp. 66\u201377 (2005)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Little Engines of Proof, Invited talk, 3rd FLoC, Copenhagen (2002), http:\/\/www.csl.sri.com\/users\/shankar\/LEP.html","DOI":"10.1007\/3-540-45614-7_1"},{"issue":"1","key":"4_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combinations of Theories. J. ACM\u00a031(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"4_CR22","volume-title":"Proc. LICS-16","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proc. LICS-16. IEEE, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11559306_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:49:23Z","timestamp":1605642563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11559306_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540290513","9783540317302"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11559306_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}