{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T15:04:18Z","timestamp":1775055858513,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_51","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"504-518","source":"Crossref","is-referenced-by-count":123,"title":["Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gr\u00e9gory","family":"Th\u00e9oduloz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"51_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking C programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"51_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"51_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"key":"51_CR4","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1145\/154630.154650","volume-title":"Proc. PEPM","author":"M. Codish","year":"1993","unstructured":"Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M., Hermenegildo, M.: Improving abstract interpretations by combining domains. In: Proc. PEPM, pp. 194\u2013205. ACM Press, New York (1993)"},{"key":"51_CR5","first-page":"238","volume-title":"Proc. POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"51_CR6","first-page":"269","volume-title":"Proc. POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. POPL, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"51_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/3-540-60045-0_58","volume-title":"Computer Aided Verification","author":"P. Cousot","year":"1995","unstructured":"Cousot, P., Cousot, R.: Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 293\u2013308. Springer, Heidelberg (1995)"},{"key":"51_CR8","first-page":"554","volume-title":"Proc. ICSE","author":"M.B. Dwyer","year":"1996","unstructured":"Dwyer, M.B., Clarke, L.A.: A flexible architecture for building data-flow analyzers. In: Proc. ICSE, pp. 554\u2013564. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"51_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1145\/1081706.1081742","volume-title":"Proc. ESEC\/FSE","author":"J. Fischer","year":"2005","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Proc. ESEC\/FSE, pp. 227\u2013236. ACM Press, New York (2005)"},{"key":"51_CR10","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1145\/1133981.1134026","volume-title":"Proc. PLDI","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proc. PLDI, pp. 376\u2013386. ACM Press, New York (2006)"},{"key":"51_CR11","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"51_CR12","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1145\/503272.503298","volume-title":"Proc. POPL","author":"S. Lerner","year":"2002","unstructured":"Lerner, S., Grove, D., Chambers, C.: Composing data-flow analyses and transformations. In: Proc. POPL, pp. 270\u2013282. ACM Press, New York (2002)"},{"key":"51_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"51_CR14","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/s100090050017","volume":"2","author":"F. Martin","year":"1998","unstructured":"Martin, F.: PAG: An efficient program analyzer generator. STTT\u00a02, 46\u201367 (1998)","journal-title":"STTT"},{"key":"51_CR15","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.\u00a03444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"51_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"51_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS\u00a024, 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"51_CR18","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/268946.268950","volume-title":"Proc. POPL","author":"D.A. Schmidt","year":"1998","unstructured":"Schmidt, D.A.: Data-flow analysis is model checking of abstract interpretations. In: Proc. POPL, pp. 38\u201348. ACM Press, New York (1998)"},{"key":"51_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B. Steffen","year":"1991","unstructured":"Steffen, B.: Data-flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 346\u2013365. Springer, Heidelberg (1991)"},{"key":"51_CR20","first-page":"82","volume-title":"Proc. PLDI","author":"S.W.K. Tjiangan","year":"1992","unstructured":"Tjiangan, S.W.K., Hennessy, J.: SHARLIT: A tool for building optimizers. In: Proc. PLDI, pp. 82\u201393. ACM Press, New York (1992)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_51.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T23:24:46Z","timestamp":1684020286000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","relation":{},"subject":[]}}