{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:07:37Z","timestamp":1769731657708,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642331244","type":"print"},{"value":"9783642331251","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_22","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T06:47:24Z","timestamp":1346222844000},"page":"317-333","source":"Crossref","is-referenced-by-count":16,"title":["Satisfiability Solvers Are Static Analysers"],"prefix":"10.1007","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203\u2013213. ACM Press (2001)","DOI":"10.1145\/381694.378846"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proc. of Software Testing and Analysis, pp. 3\u201314. ACM Press (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM\u00a050, 752\u2013794 (2003)","journal-title":"JACM"},{"key":"22_CR4","unstructured":"Cousot, P.: Abstract interpretation. MIT Course 16.399 (February-May 2005)"},{"key":"22_CR5","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 Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"issue":"2-3","key":"22_CR7","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming\u00a013(2-3), 103\u2013179 (1992)","journal-title":"Journal of Logic Programming"},{"issue":"4","key":"22_CR8","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-19805-2_31","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The Reduced Product of Abstract Domains and the Combination of Decision Procedures. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 456\u2013472. Springer, Heidelberg (2011)"},{"key":"22_CR10","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. CACM\u00a05, 394\u2013397 (1962)","journal-title":"CACM"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM\u00a07, 201\u2013215 (1960)","journal-title":"JACM"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric Bounds Analysis with Conflict-Driven Learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P. Granger","year":"1992","unstructured":"Granger, P.: Improving the Results of Static Analyses Programs by Local Decreasing Iteration (Extended Abstract). In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol.\u00a0652, pp. 68\u201379. Springer, Heidelberg (1992)"},{"key":"22_CR14","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":"22_CR15","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/567446.567454","volume-title":"POPL","author":"L.H. Holley","year":"1980","unstructured":"Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: POPL, pp. 68\u201382. ACM Press, New York (1980)"},{"key":"22_CR16","first-page":"194","volume-title":"POPL","author":"G.A. Kildall","year":"1973","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: POPL, pp. 194\u2013206. ACM, New York (1973)"},{"key":"22_CR17","unstructured":"King, J.C.: A Program Verifier. PhD thesis (1969)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 104\u2013118. Springer, Heidelberg (2010)"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). JACM\u00a053, 937\u2013977 (2006)","journal-title":"JACM"},{"issue":"5","key":"22_CR20","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X. Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. TOPLAS\u00a029(5), 26 (2007)","journal-title":"TOPLAS"},{"issue":"1","key":"22_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM\u00a012(1), 23\u201341 (1965)","journal-title":"JACM"},{"key":"22_CR22","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP \u2013 a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227 (1996)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing Learned Clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-642-33125-1_23","volume-title":"SAS 2012","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Generalization of St\u00e5lmarck\u2019s Method. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 334\u2013351. Springer, Heidelberg (2012)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Method for Symbolic Computation of Abstract Operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 174\u2013192. Springer, Heidelberg (2012)"},{"key":"22_CR26","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/103135.103136","volume":"13","author":"M.N. Wegman","year":"1991","unstructured":"Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. TOPLAS\u00a013, 181\u2013210 (1991)","journal-title":"TOPLAS"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:11:20Z","timestamp":1606187480000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}