{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T23:49:44Z","timestamp":1725752984238},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_28","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T05:11:19Z","timestamp":1382332279000},"page":"431-446","source":"Crossref","is-referenced-by-count":1,"title":["Reconstructing Paths for Reachable Code"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Arlt","sequence":"first","affiliation":[]},{"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-27940-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 39\u201355. Springer, Heidelberg (2012)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1007\/978-3-642-31424-7_62","volume-title":"Computer Aided Verification","author":"S. Arlt","year":"2012","unstructured":"Arlt, S., Sch\u00e4f, M.: Joogie: Infeasible Code Detection for Java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 767\u2013773. Springer, Heidelberg (2012)"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108768.1108813","volume":"31","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes\u00a031, 82\u201387 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-27705-4_24","volume-title":"Verified Software: Theories, Tools, Experiments","author":"C. Bertolini","year":"2012","unstructured":"Bertolini, C., Sch\u00e4f, M., Schweitzer, P.: Infeasible Code Detection. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 310\u2013325. Springer, Heidelberg (2012)"},{"unstructured":"Christ, J., Hoenicke, J., Sch\u00e4f, M.: Towards Bounded Infeasible Code Detection. CoRR, abs\/1205.6527 (2012)","key":"28_CR5"},{"key":"28_CR6","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":"28_CR7","volume-title":"A discipline of programming \/ Edsger W. Dijkstra","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of programming \/ Edsger W. Dijkstra. Prentice-Hall, Englewood Cliffs (1976)"},{"doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI, pp. 435\u2013445 (2007)","key":"28_CR8","DOI":"10.1145\/1273442.1250784"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"A.F. Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 351\u2013368. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: SOSP, pp. 57\u201372 (2001)","key":"28_CR10","DOI":"10.21236\/ADA419584"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. SIGPLAN Not., 234\u2013245 (2002)","key":"28_CR11","DOI":"10.1145\/543552.512558"},{"doi-asserted-by":"crossref","unstructured":"Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: FTfJP, pp. 6:1\u20136:7 (2009)","key":"28_CR12","DOI":"10.1145\/1557898.1557904"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-05089-3_22","volume-title":"FM 2009: Formal Methods","author":"J. Hoenicke","year":"2009","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: It\u2019s Doomed; We Can Prove It. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 338\u2013353. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: Doomed Program Points. Formal Methods in System Design (2010)","key":"28_CR14","DOI":"10.1007\/s10703-010-0102-0"},{"doi-asserted-by":"crossref","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. In: OOPSLA, pp. 132\u2013136 (2004)","key":"28_CR15","DOI":"10.1145\/1028664.1028717"},{"doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS, pp. 23\u201330 (2007)","key":"28_CR16","DOI":"10.1145\/1292316.1292319"},{"doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett., 281\u2013288 (2005)","key":"28_CR17","DOI":"10.1016\/j.ipl.2004.10.015"},{"doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program, 209\u2013226 (2005)","key":"28_CR18","DOI":"10.1016\/j.scico.2004.05.016"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"28_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA, pp. 287\u2013297 (2012)","key":"28_CR21","DOI":"10.1145\/2338965.2336788"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T19:58:26Z","timestamp":1558641506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}