{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:15:44Z","timestamp":1725747344979},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410352"},{"type":"electronic","value":"9783642410369"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41036-9_4","type":"book-chapter","created":{"date-parts":[[2013,9,3]],"date-time":"2013-09-03T05:49:49Z","timestamp":1378187389000},"page":"23-44","source":"Crossref","is-referenced-by-count":4,"title":["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"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-39910-0_3","volume-title":"Verification: Theory and Practice","author":"R. Alur","year":"2004","unstructured":"Alur, R.: Formal analysis of hierarchical state machines. In: Dershowitz, N. (ed.) Verification (Manna Festschrift). LNCS, vol.\u00a02772, pp. 42\u201366. Springer, Heidelberg (2004)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-31424-7_19","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 210\u2013226. Springer, Heidelberg (2012)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"Computer Aided Verification","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 366\u2013378. Springer, Heidelberg (2007)"},{"key":"4_CR5","unstructured":"Ball, T., Bounimova, E., Levin, V., de Moura, L.: Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. Technical Report MSR-TR-2010-24, Microsoft Research (2010)"},{"issue":"7","key":"4_CR6","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":"4_CR7","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (2001)","DOI":"10.1145\/378795.378846"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: SPIN, pp. 113\u2013130 (2000)","DOI":"10.1007\/10722468_7"},{"key":"4_CR9","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":"4_CR10","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Program Analysis for Software Tools and Engineering (2005)","DOI":"10.1145\/1108792.1108813"},{"key":"4_CR11","unstructured":"Barnett, M., Qadeer, S.: BCT: A translator from MSIL to Boogie. In: Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (2012)"},{"key":"4_CR12","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT (2012)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N. Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol.\u00a07935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"key":"4_CR14","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":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-33125-1_29","volume-title":"Static Analysis","author":"M. Emmi","year":"2012","unstructured":"Emmi, M., Lal, A.: Finding non-terminating executions in distributed asynchronous programs. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 439\u2013455. Springer, Heidelberg (2012)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Emmi, M., Lal, A., Qadeer, S.: Asynchronous programs with prioritized task-buffers. In: Foundations of Software Engineering (2012)","DOI":"10.1145\/2393596.2393652"},{"key":"4_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":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-36742-7_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Godefroid","year":"2013","unstructured":"Godefroid, P., Yannakakis, M.: Analysis of boolean programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 214\u2013229. Springer, Heidelberg (2013)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: Foundations of Software Engineering (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"4_CR21","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":"4_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: Revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 493\u2013508. Springer, Heidelberg (2009)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 475\u2013478. Springer, Heidelberg (2004)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"4_CR26","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"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Computer and System Sciences\u00a021, 317\u2013353 (1980)","journal-title":"J. Computer and System Sciences"},{"key":"4_CR28","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann (1997)"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: International Conference on Software Engineering, pp. 355\u2013364 (2010)","DOI":"10.1145\/1806799.1806852"},{"issue":"4","key":"4_CR30","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R. Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning\u00a044(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Programming Language Design and Implementation, pp. 14\u201324 (2004)","DOI":"10.1145\/996893.996845"},{"key":"4_CR32","unstructured":"Rakamaric, Z., Emmi, M.: SMACK: Static Modular Assertion ChecKer, \n                  \n                    http:\/\/smackers.github.io\/smack"},{"key":"4_CR33","unstructured":"Sinha, N.: Modular bug detection with inertial refinement. In: FMCAD (2010)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Wang, R., Chen, S., Wang, X., Qadeer, S.: How to shop for free online \u2014 security analysis of Cashier-as-a-Service based web stores. In: IEEE Symposium on Security and Privacy, pp. 465\u2013480 (2011)","DOI":"10.1109\/SP.2011.26"},{"key":"4_CR35","unstructured":"Wang, R., Zhou, Y., Chen, S., Qadeer, S., Evans, D., Gurevich, Y.: Explicating SDKs: Uncovering assumptions underlying secure authentication and authorization. In: USENIX Security Symposium (2013)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41036-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:24:56Z","timestamp":1558041896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41036-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410352","9783642410369"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41036-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}