{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:39:35Z","timestamp":1742981975635,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466681"},{"type":"electronic","value":"9783662466698"}],"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-46669-8_25","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:37:37Z","timestamp":1427899057000},"page":"610-633","source":"Crossref","is-referenced-by-count":8,"title":["Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement"],"prefix":"10.1007","author":[{"given":"Tachio","family":"Terauchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI, pp. 405\u2013416. ACM (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 331\u2013344. ACM (2011)","DOI":"10.1145\/1925844.1926424"},{"key":"25_CR3","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":"25_CR4","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 471\u2013482. ACM (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"25_CR9","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)"},{"issue":"1","key":"25_CR10","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theoretical Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Computer Science"},{"key":"25_CR11","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":"25_CR12","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":"25_CR13","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":"25_CR14","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Albert, E., Mu, S. (eds.) PEPM, pp. 53\u201362. ACM (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"25_CR15","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley (1998)"},{"issue":"3-4","key":"25_CR16","first-page":"141","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisability modulo theories. JSAT\u00a03(3-4), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1707801.1706315"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Unno, H.: Relaxed stratification: A new approach to practical complete predicate refinement (2015), \n                    \n                      http:\/\/www.jaist.ac.jp\/~terauchi","DOI":"10.1007\/978-3-662-46669-8_25"},{"issue":"115-125","key":"25_CR19","first-page":"10","volume":"2","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Porto, A., L\u00f3pez-Fraguas, F.J. (eds.) PPDP, pp. 277\u2013288. ACM (2009)","DOI":"10.1145\/1599410.1599445"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free horn clauses via sampling. In: TACAS (2015) (to appear)","DOI":"10.1007\/978-3-662-46681-0_10"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 75\u201386. ACM (2013)","DOI":"10.1145\/2480359.2429081"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:21:49Z","timestamp":1559139709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}