{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:23:39Z","timestamp":1725899019752},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_42","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"599-615","source":"Crossref","is-referenced-by-count":13,"title":["Alternate and Learn: Finding Witnesses without Looking All over"],"prefix":"10.1007","author":[{"given":"Nishant","family":"Sinha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nimit","family":"Singhania","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Satish","family":"Chandra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manu","family":"Sridharan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","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":"42_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"42_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: PLDI, pp. 363\u2013374 (2009)","DOI":"10.1145\/1543135.1542517"},{"key":"42_CR5","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"42_CR7","first-page":"1","volume":"8","author":"A. Griggio","year":"2012","unstructured":"Griggio, A.: A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT\u00a08, 1\u201327 (2012)","journal-title":"JSAT"},{"key":"42_CR8","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: POPL (2007)","DOI":"10.1145\/1190216.1190258"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002 (2002)","DOI":"10.1145\/503272.503279"},{"key":"42_CR10","doi-asserted-by":"crossref","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. In: OOPSLA Companion (2004)","DOI":"10.1145\/1028664.1028717"},{"key":"42_CR11","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, pp. 133\u2013142 (2011)","DOI":"10.1109\/ASE.2011.6100046"},{"key":"42_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"issue":"6","key":"42_CR13","first-page":"645","volume":"33","author":"A. K\u00f6lbl","year":"2005","unstructured":"K\u00f6lbl, A., Pixley, C.: Constructing efficient formal models from high-level descriptions using symbolic simulation. IJPP\u00a033(6), 645\u2013666 (2005)","journal-title":"IJPP"},{"key":"42_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-20398-5_18","volume-title":"NASA Formal Methods","author":"S.K. Lahiri","year":"2011","unstructured":"Lahiri, S.K., Qadeer, S.: Call Invariants. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 237\u2013251. Springer, Heidelberg (2011)"},{"key":"42_CR15","series-title":"LNCS","first-page":"427","volume-title":"CAV 2012","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.: Corral: 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":"42_CR16","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, pp. 213\u2013224 (2008)","DOI":"10.1145\/1390630.1390657"},{"key":"42_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-23702-7_11","volume-title":"Static Analysis","author":"K.-K. Ma","year":"2011","unstructured":"Ma, K.-K., Yit Phang, K., Foster, J.S., Hicks, M.: Directed Symbolic Execution. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 95\u2013111. Springer, Heidelberg (2011)"},{"key":"42_CR18","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":"42_CR19","first-page":"49","volume-title":"POPL","author":"T. Reps","year":"1995","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49\u201361. ACM, NY (1995)"},{"key":"42_CR20","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedureal data flow analysis. In: Program Flow Analysis: Theory and Applications, vol.\u00a05, pp. 189\u2013234. Prentice Hall (1981)"},{"key":"42_CR21","doi-asserted-by":"crossref","unstructured":"Sinha, N.: Symbolic program analysis using term rewriting, generalization. In: FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.23"},{"key":"42_CR22","unstructured":"Sinha, N.: Modular bug detection with inertial refinement. In: FMCAD (2010)"},{"key":"42_CR23","unstructured":"Sinha, N., Singhania, N., Chandra, S., Sridharan, M.: Scalable bug detection via alternating scope expansion and pertinent scope learning. IBM Technical Report RI12003 (2012)"},{"issue":"1","key":"42_CR24","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10515-006-0005-x","volume":"14","author":"M. Taghdiri","year":"2007","unstructured":"Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Autom. Softw. Eng.\u00a014(1), 87\u2013121 (2007)","journal-title":"Autom. Softw. Eng."}],"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_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:00:02Z","timestamp":1620129602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}