{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:36:30Z","timestamp":1743100590374,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_10","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"149-163","source":"Crossref","is-referenced-by-count":10,"title":["Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling"],"prefix":"10.1007","author":[{"given":"Hiroshi","family":"Unno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-39799-8_22","volume-title":"Computer Aided Verification","author":"A. Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 313\u2013329. Springer, Heidelberg (2013)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N. Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol.\u00a07935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"issue":"03","key":"10_CR3","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. a new form of the herbrand-gentzen theorem. The Journal of Symbolic Logic\u00a022(03), 250\u2013268 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416. ACM (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp. 331\u2013344. ACM (2011)","DOI":"10.1145\/1925844.1926424"},{"key":"10_CR6","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":"10_CR7","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the grey area of proofs. In: POPL, pp. 259\u2013272. ACM (2012)","DOI":"10.1145\/2103621.2103689"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-54833-8_21","volume-title":"Programming Languages and Systems","author":"T. Kuwahara","year":"2014","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol.\u00a08410, pp. 392\u2013411. Springer, Heidelberg (2014)"},{"key":"10_CR11","unstructured":"McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical Report MSR-TR-2013-6 (January 2013)"},{"key":"10_CR12","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":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54108-7_1","volume-title":"Verified Software: Theories, Tools, Experiments","author":"P. R\u00fcmmer","year":"2014","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 1\u201321. Springer, Heidelberg (2014)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P. R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: PEPM, pp. 53\u201362. ACM (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"10_CR16","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley (1998)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-31424-7_11","volume-title":"Computer Aided Verification","author":"R. Sharma","year":"2012","unstructured":"Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 71\u201387. Springer, Heidelberg (2012)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1707801.1706315"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Unno, H.: Relaxed stratification: A new approach to practical complete predicate refinement. In: ESOP (2015) (to appear)","DOI":"10.1007\/978-3-662-46669-8_25"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP, pp. 277\u2013288. ACM (2009)","DOI":"10.1145\/1599410.1599445"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free horn clauses via sampling. In: 2015, \n                      \n                        http:\/\/www.cs.tsukuba.ac.jp\/~uhiro","DOI":"10.1007\/978-3-662-46681-0_10"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: POPL, pp. 75\u201386. ACM (2013)","DOI":"10.1145\/2480359.2429081"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:11:58Z","timestamp":1559139118000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}