{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:15:25Z","timestamp":1766135725647},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_23","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T04:44:25Z","timestamp":1132634665000},"page":"322-336","source":"Crossref","is-referenced-by-count":21,"title":["Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[]},{"given":"Malay","family":"Ganai","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Idini, M., Maratea, M.: TSAT++: an open platform for satisfiability modulo theories. In: Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)","DOI":"10.1016\/j.entcs.2004.06.065"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D.L., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166. Springer, Heidelberg (1996)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","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. LNCS, vol.\u00a02404, p. 78. Springer, Heidelberg (2002)"},{"key":"23_CR5","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, Cambridge (1990)"},{"key":"23_CR6","unstructured":"Cotton, S.: Satisfiability checking with difference constraints. Msc thesis, IMPRS Computer Science, Saarbrucken (2005)"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"23_CR9","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)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation and Test in Europe (DATE 2003), March 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, June 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"issue":"1","key":"23_CR13","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: The small model property: How small can it be? Information and Computation\u00a0178(1), 275\u2013293 (2002)","journal-title":"Information and Computation"},{"key":"23_CR14","unstructured":"Pratt, V.R.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology (1977)"},{"issue":"3","key":"23_CR15","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/PL00009261","volume":"23","author":"G. Ramalingam","year":"1999","unstructured":"Ramalingam, G., Song, J., Joscovicz, L., Miller, R.E.: Solving difference constraints incrementally. Algorithmica\u00a023(3), 261\u2013275 (1999)","journal-title":"Algorithmica"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proceedings of the Design Automation Conference, June 2003, pp. 425\u2013430 (2003)","DOI":"10.1145\/775832.775945"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M., Sakallah, K.A.: Grasp\u2014a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, November 1996, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 209\u2013222. Springer, Heidelberg (2002)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-27813-9_12","volume-title":"Computer Aided Verification","author":"M. Talupur","year":"2004","unstructured":"Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 148\u2013161. Springer, Heidelberg (2004)"},{"key":"23_CR20","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe (DATE 2003), pp. 880\u2013885 (March 2003)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:02:27Z","timestamp":1605625347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11591191_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}