{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T01:18:28Z","timestamp":1725671908240},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_7","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"54-69","source":"Crossref","is-referenced-by-count":5,"title":["Inferring Definite Counterexamples through Under-Approximation"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Brauer","sequence":"first","affiliation":[]},{"given":"Axel","family":"Simon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97\u2013105. ACM (2003)","DOI":"10.1145\/640128.604140"},{"issue":"2","key":"7_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A. Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.R.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM\u00a053(2), 66\u201375 (2010)","journal-title":"Commun. ACM"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-15769-1_11","volume-title":"Static Analysis","author":"J. Brauer","year":"2010","unstructured":"Brauer, J., King, A.: Automatic Abstraction for Intervals Using Boolean Formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 167\u2013183. Springer, Heidelberg (2010)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-19718-5_6","volume-title":"Programming Languages and Systems","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A.: Transfer Function Synthesis without Quantifier Elimination. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 97\u2013115. Springer, Heidelberg (2011)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential Quantification as Incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-540-39910-0_9","volume-title":"Verification: Theory and Practice","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Veith, H.: Counterexamples Revisited: Principles, Algorithms, Applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 208\u2013224. Springer, Heidelberg (2004)"},{"key":"7_CR10","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, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"7_CR12","unstructured":"Erez, G.: Generating concrete counterexamples for sound abstract interpretation. Master\u2019s thesis, School of Computer Science, Tel-Aviv University, Israel (2004)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically Refining Abstract Interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"7_CR14","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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/11547662_15","volume-title":"Static Analysis","author":"Y. Jung","year":"2005","unstructured":"Jung, Y., Kim, J., Shin, J., Yi, K.: Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post Analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 203\u2013217. Springer, Heidelberg (2005)"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine Relationships among Variables of a Program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.infsof.2009.10.004","volume":"52","author":"Y. Kim","year":"2010","unstructured":"Kim, Y., Lee, J., Han, H., Choe, K.-M.: Filtering false alarms of buffer overflow analysis using SMT solvers. Inform. & Softw. Techn.\u00a052(2), 210\u2013219 (2010)","journal-title":"Inform. & Softw. Techn."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-24599-5_22","volume-title":"Logic Programming","author":"A. King","year":"2003","unstructured":"King, A., Lu, L.: Forward versus Backward Verification of Logic Programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol.\u00a02916, pp. 315\u2013330. Springer, Heidelberg (2003)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-70545-1_26","volume-title":"Computer Aided Verification","author":"A. King","year":"2008","unstructured":"King, A., S\u00f8ndergaard, H.: Inferring Congruence Equations Using SAT. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 281\u2013293. Springer, Heidelberg (2008)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-44898-5_16","volume-title":"Static Analysis","author":"T. Kremenek","year":"2003","unstructured":"Kremenek, T., Engler, D.R.: Z-ranking: Using Statistical Analysis to Counter the Impact of Static Analysis Approximations. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 295\u2013315. Springer, Heidelberg (2003)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-540-30482-1_23","volume-title":"Formal Methods and Software Engineering","author":"D. Kroning","year":"2004","unstructured":"Kroning, D., Groce, A., Clarke, E.: Counterexample Guided Abstraction Refinement Via Program Execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 224\u2013238. Springer, Heidelberg (2004)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A Symbolic Approach to Predicate Abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-27940-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W. Lee","year":"2012","unstructured":"Lee, W., Lee, W., Yi, K.: Sound Non-statistical Clustering of Static Analysis Alarms. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 299\u2013314. Springer, Heidelberg (2012)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11562931_15","volume-title":"Logic Programming","author":"M.J. Maher","year":"2005","unstructured":"Maher, M.J.: Abduction of Linear Arithmetic Constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 174\u2013188. Springer, Heidelberg (2005)"},{"key":"7_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-540-89439-1_30","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M.J. Maher","year":"2008","unstructured":"Maher, M.J., Huang, G.: On Computing Constraint Abduction Answers. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 421\u2013435. Springer, Heidelberg (2008)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of Modular Arithmetic. ACM Trans. Program. Lang. Syst.\u00a029(5) (August 2007)","DOI":"10.1145\/1275497.1275504"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X. Rival","year":"2005","unstructured":"Rival, X.: Understanding the Origin of Alarms in Astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 303\u2013319. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:26Z","timestamp":1620126866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}