{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:17:26Z","timestamp":1770977846226,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_32","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"427-443","source":"Crossref","is-referenced-by-count":100,"title":["A Solver for Reachability Modulo Theories"],"prefix":"10.1007","author":[{"given":"Akash","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Babic, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: ICSE, pp. 211\u2013220 (2008)","DOI":"10.1145\/1368088.1368118"},{"issue":"7","key":"32_CR2","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM\u00a054(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE, pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"32_CR5","unstructured":"Barnett, M., Qadeer, S.: BCT: A translator from MSIL to Boogie. In: Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (2012)"},{"key":"32_CR6","unstructured":"Beyer, D. (ed.): 1st International Competition on Software Verification, co-located with TACAS 2012, Tallinn, Estonia (2012)"},{"key":"32_CR7","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-642-13754-9_4","volume-title":"Pnueli Festschrift","author":"E.M. Clarke","year":"2010","unstructured":"Clarke, E.M., Kurshan, R.P., Veith, H.: The Localization Reduction and Counterexample-Guided Abstraction Refinement. In: Manna, Z., Peled, D.A. (eds.) Pnueli Festschrift. LNCS, vol.\u00a06200, pp. 61\u201371. Springer, Heidelberg (2010)"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (2009)","DOI":"10.1145\/1480881.1480921"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Transactions on Software Engineering (2011)","DOI":"10.1145\/1810295.1810396"},{"key":"32_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"32_CR14","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Principles of Programming Languages (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages (2002)","DOI":"10.1145\/503272.503279"},{"key":"32_CR19","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2003)"},{"key":"32_CR20","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley (1999)"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Balakrishnan, G., Gupta, A., Sankaranarayanan, S., Maeda, N., Tokuoka, H., Imoto, T., Miyazaki, Y.: DC2: A framework for scalable, scope-bounded software verification. In: ASE (2011)","DOI":"10.1109\/ASE.2011.6100046"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: PLDI (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"32_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-02658-4_38","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 509\u2013524. Springer, Heidelberg (2009)"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., Lahiri, S.: Corral: A solver for reachability modulo theories. Technical Report MSR-TR-2012-09, Microsoft Research (2012)","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design\u00a035(1) (2009)","DOI":"10.1007\/s10703-009-0078-9"},{"issue":"1","key":"32_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Loginov, A., Yahav, E., Chandra, S., Fink, S., Rinetzky, N., Nanda, M.G.: Verifying dereference safety via expanding-scope analysis. In: ISSTA (2008)","DOI":"10.1145\/1390630.1390657"},{"key":"32_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 104\u2013118. Springer, Heidelberg (2010)"},{"key":"32_CR29","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: ICSE, pp. 355\u2013364 (2010)","DOI":"10.1145\/1806799.1806852"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"32_CR31","unstructured":"Sinha, N.: Modular bug detection with inertial refinement. In: FMCAD (2010)"},{"key":"32_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-27705-4_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Vujo\u0161evi\u0107-Jani\u010di\u0107","year":"2012","unstructured":"Vujo\u0161evi\u0107-Jani\u010di\u0107, M., Kuncak, V.: Development and Evaluation of LAV: An SMT-Based Error Finding Platform. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 98\u2013113. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:56Z","timestamp":1620129596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}