{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:25Z","timestamp":1780994485142,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662534120","type":"print"},{"value":"9783662534137","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-53413-7_6","type":"book-chapter","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T11:57:11Z","timestamp":1472558231000},"page":"105-125","source":"Crossref","is-referenced-by-count":4,"title":["Bounded Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Maria","family":"Christakis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-15057-9_1","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T Ball","year":"2010","unstructured":"Ball, T., Hackett, B., Lahiri, S.K., Qadeer, S., Vanegue, J.: Towards scalable modular checking of user-defined properties. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 1\u201324. Springer, Heidelberg (2010)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking. CoRR, abs\/1109.6926 (2011)","DOI":"10.1145\/2393596.2393664"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: FSE, pp. 57\u201367. ACM (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"6_CR5","unstructured":"Christakis, M.: Narrowing the gap between verification and systematic testing. Ph.D. thesis, ETH Zurich (2015)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-642-32759-9_13","volume-title":"FM 2012: Formal Methods","author":"M Christakis","year":"2012","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 132\u2013146. Springer, Heidelberg (2012)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-662-46081-8_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Christakis","year":"2015","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: An experimental evaluation of deliberate unsoundness in a static program analyzer. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 336\u2013354. Springer, Heidelberg (2015)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: ICSE. ACM (2016, to appear)","DOI":"10.1145\/2884781.2884843"},{"key":"6_CR9","first-page":"7","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19, 7\u201334 (2001)","journal-title":"FMSD"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"6_CR11","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":"6_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","first-page":"324","volume-title":"Computer Aided Verification","author":"A Das","year":"2015","unstructured":"Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324\u2013342. Springer, Heidelberg (2015)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: POPL, pp. 143\u2013154. ACM (2013)","DOI":"10.1145\/2429069.2429087"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: SAC, pp. 2103\u20132110. ACM (2010)","DOI":"10.1145\/1774088.1774531"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: POPL, pp. 261\u2013273. ACM (2015)","DOI":"10.1145\/2676726.2676987"},{"key":"6_CR18","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47, 361\u2013416 (2000)","journal-title":"J. ACM"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 3672, pp. 203\u2013217. Springer, Heidelberg (2005)"},{"key":"6_CR23","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. CACM 19, 385\u2013394 (1976)","journal-title":"CACM"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 2694, pp. 295\u2013315. Springer, Heidelberg (2003)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-319-21690-4_22","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2015","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: Fine-grained caching of verification results. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380\u2013397. Springer, Heidelberg (2015)"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: towards usable verification. In: PLDI, pp. 294\u2013304. ACM (2014)","DOI":"10.1145\/2666356.2594326"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"6_CR28","unstructured":"Do, L.N.Q., Ali, K., Bodden, E., Livshits, B.: Toward a just-in-time static analysis. Technical Report TUD-CS-2015-1167, Technische Universit\u00e4t Darmstadt (2015)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Sadowski, C., van Gogh, J., Jaspan, C., S\u00f6derberg, E., Winter, C., Tricorder: building a program analysis ecosystem. In: ICSE, pp. 598\u2013608. IEEE Computer Society (2015)","DOI":"10.1109\/ICSE.2015.76"},{"key":"6_CR30","unstructured":"W\u00fcstholz, V.: Partial verification results. Ph.D. thesis, ETH Zurich (2015)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53413-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,19]],"date-time":"2023-08-19T22:12:32Z","timestamp":1692483152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-53413-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662534120","9783662534137"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53413-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}