{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:08:09Z","timestamp":1725505689073},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787990"},{"type":"electronic","value":"9783540788003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_33","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:26:19Z","timestamp":1207124779000},"page":"443-458","source":"Crossref","is-referenced-by-count":54,"title":["Automatically Refining Abstract Interpretations"],"prefix":"10.1007","author":[{"given":"Bhargav S.","family":"Gulavani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aditya V.","family":"Nori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Apron. Numerical Abstract Domain Library, http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P., Zaffanella, E.: Widening operators for powerset domains. Technical Report 344, University of Parma, Italy (2004)","DOI":"10.1007\/978-3-540-24622-0_13"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening opertors for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300\u2013309 (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"33_CR6","unstructured":"CIL. Infrastructure for C Program Analysis and Transformation. http:\/\/manju.cs.berkeley.edu\/cil\/"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: ESEC\/SIGSOFT FSE, pp. 227\u2013236 (2005)","DOI":"10.1145\/1081706.1081742"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"33_CR11","unstructured":"B.\u00a0S. Gulavani, S.\u00a0Chakraborty, A.\u00a0V. Nori, and S.\u00a0K. Rajamani. Automatically refining abstract interpretations. Technical Report TR-07-23, CFDVS, IIT Bombay, 2007. http:\/\/www.cfdvs.iitb.ac.in\/~bhargav\/dagger.html"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"issue":"2","key":"33_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. FMSD\u00a011(2), 157\u2013185 (1997)","journal-title":"FMSD"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/11817963_15","volume-title":"Computer Aided Verification","author":"H. Jain","year":"2006","unstructured":"Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 137\u2013151. Springer, Heidelberg (2006)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Rybalchenko, A., Podelski, A.: Armc: The logical choice for software model checking with abstraction refinement. In: PADL (2007)","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-73368-3_40","volume-title":"Computer Aided Verification","author":"C. Wang","year":"2007","unstructured":"Wang, C., Yang, Z., Gupta, A., Ivancic, F.: Using counterexamples for improving the precision of reachability computation with polyhedra. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 352\u2013365. Springer, Heidelberg (2007)"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. In: FSE, pp. 97\u2013106 (2004)","DOI":"10.1145\/1029894.1029911"}],"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\/978-3-540-78800-3_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:22:51Z","timestamp":1619522571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_33","relation":{},"subject":[]}}