{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:29:55Z","timestamp":1743038995640,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540330561"},{"type":"electronic","value":"9783540330578"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691372_9","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:22:26Z","timestamp":1143555746000},"page":"135-150","source":"Crossref","is-referenced-by-count":5,"title":["SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver"],"prefix":"10.1007","author":[{"given":"Malay K","family":"Ganai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muralidhar","family":"Talupur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics (1954)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. In: Proc. of Formal Techniques in Real-Time and Fault Tolerant Systems (2002)","DOI":"10.1007\/3-540-45739-9_15"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Adams, J., Balas, E., Zawack, D.: The shifting bottleneck procedure for job shop scheduling. In: Management Science (1988)","DOI":"10.1287\/mnsc.34.3.391"},{"key":"9_CR4","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":"Filliatre, 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, p. 246. Springer, Heidelberg (2001)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Parthasarathy, G., Iyer, M.K., Cheng, K.-T., Wang, C.: An Efficient Finite-Domain Constraint Solver for RTL Circuits. In: Proceedings of DAC (2004)","DOI":"10.1145\/996566.996628"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607. Springer, Heidelberg (1992)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kr\u00f6ning","year":"2004","unstructured":"Kr\u00f6ning, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-based satisfiability solving of presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"9_CR8","unstructured":"Bik, A.J.C., Wijshoff, H.A.G.: Implementation of Fourier-Motzkin Elimination. In: Technical Report 94-42, Dept. of Computer Science, Leiden University (1994)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 17. Springer, Heidelberg (2002)"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The Small Model Property: How small can it be? Information and computation\u00a0178(1), 279\u2013293 (2002)","journal-title":"Information and computation"},{"key":"9_CR11","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, p. 209. Springer, Heidelberg (2002)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023717","volume-title":"Computer-Aided Verification","author":"R.E. Bryant","year":"1991","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: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531. Springer, Heidelberg (1991)"},{"key":"9_CR13","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 DAC (2003)","DOI":"10.1145\/775944.775945"},{"key":"9_CR14","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via Boolean and peudo-Boolean encodings. In: Workshop on Constraints in Formal Verification (2002)"},{"key":"9_CR15","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 Combination of Theories with Equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166. Springer, Heidelberg (1996)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Idini, M., Maratea, M.: TSAT++: An Open Platform for Satisfiability Modulo Theories. In: Proceedings of Pragmatics of Decision Procedures in Automated Resonings, PDPAR 2004 (2004)","DOI":"10.1016\/j.entcs.2004.06.065"},{"key":"9_CR17","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.A., van 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":"9_CR18","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)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Wang, C., Ivancic, F., Ganai, M., Gupta, A.: Deciding Separation Logic Formulae with SAT by Incremental Negative Cycle Elimination. In: Proceeding of Logic for Programming (2005)","DOI":"10.1007\/11591191_23"},{"key":"9_CR20","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":"9_CR21","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A backtrack search pseudo-Boolean solver. In: Symposium on the Theory and Applications of Satisfiability Testing, SAT (2002)"},{"key":"9_CR22","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"key":"9_CR23","unstructured":"Cotton, S.: Satisfiability Checking with Difference Constraints. In: IMPRS Computer Science, Saarbruceken (2005)"},{"key":"9_CR24","unstructured":"Pratt, V.: Two Easy Theories Whose Combination is Hard, in Technical report, MIT (1977)"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Song, J., Joscovicz, L., Miller, R.: Solving difference constraints incrementally. Alogrithmica (1999)","DOI":"10.1007\/PL00009261"},{"key":"9_CR26","unstructured":"Strichman, O.: http:\/\/iew3.techninon.ac.il\/~ofers"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Hochbaum, D.S.: Approximation Algorithms for NP-hard Problems: PWS Publishing Company (1997)","DOI":"10.1145\/261342.571216"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Cherkassky, B.V., Goldberg, E.: Negative-cycle Detection Algorithms. In: European Symposium on Algorithms (1996)","DOI":"10.1007\/3-540-61680-2_67"},{"key":"9_CR29","volume-title":"Interval Analysis","author":"R.E. Moore","year":"1966","unstructured":"Moore, R.E.: Interval Analysis. Prentice-Hall, NJ (1966)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Hickey, T., Ju, Q., Emden, H.V.: Interval Arithmetic: from principles to implementation. Journal of the ACM (2001)","DOI":"10.1145\/502102.502106"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691372_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T21:49:22Z","timestamp":1683409762000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11691372_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}