{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:09Z","timestamp":1750810209273,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_11","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"164-170","source":"Crossref","is-referenced-by-count":0,"title":["How to Get More Out of Your Oracles"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim S.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comp. Sci. 21, 827\u2013859 (2011)","journal-title":"Math. Struct. Comp. Sci."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving","year":"2013","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): ITP 2013. LNCS, vol. 7998. Springer, Heidelberg (2013)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Claret, G., Gonz\u00e1lez-Huesca, L., R\u00e9gis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy et al. [3], pp. 67\u201383","DOI":"10.1007\/978-3-642-39634-2_8"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1016\/j.jcss.2015.11.014","volume":"82","author":"M Codish","year":"2016","unstructured":"Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Sorting nine inputs requires twenty-five comparisons. J. Comput. Syst. Sci. 82(3), 551\u2013563 (2016)","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Larsen, K.S., Schneider-Kamp, P.: Formally proving size optimality of sorting networks. J. Autom. Reason. Accepted for publication. doi:10.1007\/s10817-017-9405-9","DOI":"10.1007\/s10817-017-9405-9"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-662-54577-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_7"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Formally proving the boolean triples conjecture. In: Eiter, T., Sands, D. (eds.) LPAR-21. EPiC Series in Computing, vol. 46, pp. 509\u2013522. EasyChair Publications (2017)","DOI":"10.29007\/jvdj"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-30142-4_5","volume-title":"Theorem Proving in Higher Order Logics","author":"L Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Wiedijk, F.: Hierarchical reflection. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 66\u201381. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-30142-4_5"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260\u2013274. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14808-8_18"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38856-9_19","volume-title":"Static Analysis","author":"A Fouilh\u00e9","year":"2013","unstructured":"Fouilh\u00e9, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 345\u2013365. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38856-9_19"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_15"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Cham (2014). doi:10.1007\/978-3-319-09284-3_17"},{"issue":"7","key":"11_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Benzm\u00fcller, C., Paleo, B. (eds.) UITP, EPTCS, vol. 167, pp. 61\u201372 (2014)","DOI":"10.4204\/EPTCS.167.8"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy et al. [3], pp. 229\u2013244","DOI":"10.1007\/978-3-642-39634-2_18"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:38:58Z","timestamp":1750808338000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}