{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:15Z","timestamp":1774063035663,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642388552","type":"print"},{"value":"9783642388569","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_8","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T04:05:28Z","timestamp":1371269128000},"page":"105-125","source":"Crossref","is-referenced-by-count":87,"title":["On Solving Universally Quantified Horn Clauses"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[]},{"given":"Ken","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 46\u201361. Springer, Heidelberg (2012)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"8_CR4","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as Satisfiability Modulo Theories. In: SMT (2012)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification (Manna Festschrift). LNCS, vol.\u00a02772, pp. 243\u2013268. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-39910-0_11"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052(3) (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-36575-3_14","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C.: Automatic software model checking using clp. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 189\u2013203. Springer, Heidelberg (2003)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/503272.503291"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 235\u2013246. ACM (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-25318-8_16","volume-title":"Programming Languages and Systems","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free Horn clauses over LI+UIF. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 188\u2013203. Springer, Heidelberg (2011)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44898-5_8","volume-title":"Static Analysis","author":"M. Hermenegildo","year":"2003","unstructured":"Hermenegildo, M., Puebla, G., Bueno, F., L\u00f3pez-Garc\u00eda, P.: Program development using abstract interpretation (and the ciao system preprocessor). In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 127\u2013152. Springer, Heidelberg (2003)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K. Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-25324-9_1","volume-title":"Advances in Artificial Intelligence","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Case studies on invariant generation using a saturation theorem prover. In: Batyrshin, I., Sidorov, G. (eds.) MICAI 2011, Part I. LNCS, vol.\u00a07094, pp. 1\u201315. Springer, Heidelberg (2011)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H. Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems - tool paper. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 247\u2013251. Springer, Heidelberg (2012)"},{"issue":"20","key":"8_CR20","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. J. Log. Program.\u00a019(20), 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J. Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: Tracer: A symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 758\u2013766. Springer, Heidelberg (2012)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/11562931_34","volume-title":"Logic Programming","author":"J. Jaffar","year":"2005","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: Modeling Systems in CLP. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 412\u2013413. Springer, Heidelberg (2005)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.: Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-Based Array Invariant Generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1) (2005)","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"8_CR27","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":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"8_CR29","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD (2011)"},{"key":"8_CR30","unstructured":"McMillan, K.L., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research (2013), http:\/\/research.microsoft.com\/apps\/pubs\/?id=180055"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_24"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T14:46:09Z","timestamp":1563201969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}