{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:51:00Z","timestamp":1781927460995,"version":"3.54.5"},"publisher-location":"Cham","reference-count":201,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030591519","type":"print"},{"value":"9783030591526","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-59152-6_2","type":"book-chapter","created":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:02:35Z","timestamp":1602457355000},"page":"25-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verified Textbook Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4263-6571","authenticated-orcid":false,"given":"Manuel","family":"Eberl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4306-869X","authenticated-orcid":false,"given":"Maximilian P. L.","family":"Haslbeck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"key":"2_CR1","unstructured":"Archive of Formal Proofs. \nhttp:\/\/www.isa-afp.org"},{"key":"2_CR2","unstructured":"Abdulaziz, M., Mehlhorn, K., Nipkow, T.: Trustworthy graph algorithms (invited talk). In: Rossmanith, P., Heggernes, P., Katoen, J. (eds.) 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019. LIPIcs, vol. 138, pp. 1:1\u20131:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.1"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press (1996). \nhttps:\/\/doi.org\/10.1017\/CBO9780511624162","DOI":"10.1017\/CBO9780511624162"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/3-540-44880-2_27","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J-R Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D., M\u00e9ry, D.: Formal derivation of spanning trees algorithms. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457\u2013476. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44880-2_27"},{"issue":"4","key":"2_CR5","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1017\/S0956796800000885","volume":"3","author":"S Adams","year":"1993","unstructured":"Adams, S.: Efficient sets - a balancing act. J. Funct. Program. 3(4), 553\u2013561 (1993). \nhttps:\/\/doi.org\/10.1017\/S0956796800000885","journal-title":"J. Funct. Program."},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.6092\/issn.1972-5787\/8124","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Form. Reasoning 11(1), 43\u201376 (2018). \nhttps:\/\/doi.org\/10.6092\/issn.1972-5787\/8124","journal-title":"J. Form. Reasoning"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, LNCS, vol. 10001. Springer, Cham (2016), \nhttps:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-30494-4_4","volume-title":"Formal Methods in Computer-Aided Design","author":"B Akbarpour","year":"2004","unstructured":"Akbarpour, B., Tahar, S.: A methodology for the formal verification of FFT algorithms in HOL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 37\u201351. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30494-4_4"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-66107-0_3","volume-title":"Interactive Theorem Proving","author":"X Allamigeon","year":"2017","unstructured":"Allamigeon, X., Katz, R.D.: A formalization of convex polyhedra based on the simplex method. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 28\u201345. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_3"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2636922","volume":"11","author":"S Alstrup","year":"2014","unstructured":"Alstrup, S., Thorup, M., G\u00f8rtz, I.L., Rauhe, T., Zwick, U.: Union-find with constant time deletions. ACM Trans. Algorithms 11(1), 6:1\u20136:28 (2014). \nhttps:\/\/doi.org\/10.1145\/2636922","journal-title":"ACM Trans. Algorithms"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-51542-9_33","volume-title":"Algorithms and Data Structures","author":"A Andersson","year":"1989","unstructured":"Andersson, A.: Improving partial rebuilding by using simple balance criteria. In: Dehne, F., Sack, J.-R., Santoro, N. (eds.) WADS 1989. LNCS, vol. 382, pp. 393\u2013402. Springer, Heidelberg (1989). \nhttps:\/\/doi.org\/10.1007\/3-540-51542-9_33"},{"key":"2_CR12","unstructured":"Appel, A.W.: Efficient verified red-black trees (2011). \nhttps:\/\/www.cs.princeton.edu\/~appel\/papers\/redblack.pdf"},{"key":"2_CR13","unstructured":"Appel, A.W.: Verified Functional Algorithms, August 2018. \nhttps:\/\/softwarefoundations.cis.upenn.edu\/vfa-current\/index.html"},{"issue":"8","key":"2_CR14","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009). \nhttps:\/\/doi.org\/10.1016\/j.scico.2007.09.002","journal-title":"Sci. Comput. Program."},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Logic 9(1) (2007). \nhttps:\/\/doi.org\/10.1145\/1297658.1297660","DOI":"10.1145\/1297658.1297660"},{"key":"2_CR16","unstructured":"Ballarin, C.: Fast Fourier Transform. Archive of Formal Proofs, October 2005. \nhttp:\/\/isa-afp.org\/entries\/FFT.html\n\n, Formal proof development"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-89884-1_5","volume-title":"Programming Languages and Systems","author":"G Barthe","year":"2018","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.-Y.: An assertion-based program logic for probabilistic programs. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 117\u2013144. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89884-1_5"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Beckert, B., Schiffl, J., Schmitt, P.H., Ulbrich, M.: Proving JDK\u2019s dual pivot quicksort correct. In: Paskevich and Wies [160], pp. 35\u201348, \nhttps:\/\/doi.org\/10.1007\/978-3-319-72308-2_3","DOI":"10.1007\/978-3-319-72308-2_3"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-642-22944-2_29","volume-title":"Algebra and Coalgebra in Computer Science","author":"U Berger","year":"2011","unstructured":"Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog - a tool for program extraction supporting algebras and coalgebras. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 393\u2013399. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22944-2_29"},{"issue":"2","key":"2_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1026748613865","volume":"26","author":"U Berger","year":"2001","unstructured":"Berger, U., Schwichtenberg, H., Seisenberger, M.: The Warshall algorithm and Dickson\u2019s lemma: two examples of realistic program extraction. J. Autom. Reasoning 26(2), 205\u2013221 (2001). \nhttps:\/\/doi.org\/10.1023\/A:1026748613865","journal-title":"J. Autom. Reasoning"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-39185-1_2","volume-title":"Types for Proofs and Programs","author":"S Berghofer","year":"2003","unstructured":"Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 21\u201338. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-39185-1_2"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-02508-3_1","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2018","author":"Y Bertot","year":"2018","unstructured":"Bertot, Y.: Formal verification of a geometry algorithm: a quest for abstract views and symmetry in coq proofs. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 3\u201310. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-02508-3_1"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Cham (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"1\u20132","key":"2_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-005-2243-0","volume":"27","author":"M Besta","year":"2005","unstructured":"Besta, M., Stomp, F.A.: A complete mechanization of correctness of a string-preprocessing algorithm. Formal Methods Syst. Des. 27(1\u20132), 5\u201317 (2005). \nhttps:\/\/doi.org\/10.1007\/s10703-005-2243-0","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-009-9116-y","volume":"43","author":"JC Blanchette","year":"2009","unstructured":"Blanchette, J.C.: Proof pearl: Mechanizing the textbook proof of Huffman\u2019s algorithm. J. Autom. Reasoning 43(1), 1\u201318 (2009). \nhttps:\/\/doi.org\/10.1007\/s10817-009-9116-y","journal-title":"J. Autom. Reasoning"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0304-3975(80)90018-3","volume":"11","author":"N Blum","year":"1980","unstructured":"Blum, N., Mehlhorn, K.: On the average number of rebalancing operations in weight-balanced trees. Theor. Comput. Sci. 11, 303\u2013320 (1980). \nhttps:\/\/doi.org\/10.1016\/0304-3975(80)90018-3","journal-title":"Theor. Comput. Sci."},{"key":"2_CR29","unstructured":"Bobot, F.: Topological sorting (2014). \nhttp:\/\/toccata.lri.fr\/gallery\/topological_sorting.en.html\n\n, formal proof development"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-29007-8_13","volume-title":"Frontiers of Combining Systems","author":"R Bottesch","year":"2019","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: Verifying an incremental theory solver for linear arithmetic in Isabelle\/HOL. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 223\u2013239. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-29007-8_13"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73\u201378. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_6"},{"key":"2_CR32","unstructured":"Boyer, R.S., Moore, J S.: Proving theorems about LISP functions. In: Nilsson, N. (ed.) International Joint Conference on Artificial Intelligence. pp. 486\u2013493. William Kaufmann (1973) \nhttp:\/\/ijcai.org\/Proceedings\/73\/Papers\/053.pdf"},{"issue":"10","key":"2_CR33","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1145\/359842.359859","volume":"20","author":"RS Boyer","year":"1977","unstructured":"Boyer, R.S., Moore, J.S.: A fast string searching algorithm. Commun. ACM 20(10), 762\u2013772 (1977). \nhttps:\/\/doi.org\/10.1145\/359842.359859","journal-title":"Commun. ACM"},{"key":"2_CR34","volume-title":"A computational logic handbook, Perspectives in Computing","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic handbook, Perspectives in Computing, vol. 23. Academic Press, New York (1979)"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"RS Boyer","year":"2002","unstructured":"Boyer, R.S., Strother Moore, J.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 9\u201327. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45587-6_3"},{"issue":"6","key":"2_CR36","doi-asserted-by":"publisher","first-page":"839","DOI":"10.1017\/S095679680000201X","volume":"6","author":"GS Brodal","year":"1996","unstructured":"Brodal, G.S., Okasaki, C.: Optimal purely functional priority queues. J. Funct. Program. 6(6), 839\u2013857 (1996). \nhttps:\/\/doi.org\/10.1017\/S095679680000201X","journal-title":"J. Funct. Program."},{"issue":"8","key":"2_CR37","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1016\/j.comgeo.2010.06.006","volume":"45","author":"C Brun","year":"2012","unstructured":"Brun, C., Dufourd, J., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8), 436\u2013457 (2012). \nhttps:\/\/doi.org\/10.1016\/j.comgeo.2010.06.006","journal-title":"Comput. Geom."},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_14"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-44755-5_12","volume-title":"Theorem Proving in Higher Order Logics","author":"V Capretta","year":"2001","unstructured":"Capretta, V.: Certifying the fast Fourier transform with coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 154\u2013168. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44755-5_12"},{"key":"2_CR40","unstructured":"Chan, H.L.J.: Primality testing is polynomial-time: a mechanised verification of the AKS algorithm. Ph.D. thesis, Australian National University (2019). \nhttps:\/\/openresearch-repository.anu.edu.au\/bitstream\/1885\/177195\/1\/thesis.pdf"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Program verification through characteristic formulae. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming. ICFP 2010, pp. 321\u2013332. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1863543.1863590","DOI":"10.1145\/1863543.1863590"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-22102-1_9","volume-title":"Interactive Theorem Proving","author":"A Chargu\u00e9raud","year":"2015","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 137\u2013153. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-22102-1_9"},{"issue":"3","key":"2_CR43","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-017-9431-7","volume":"62","author":"A Chargu\u00e9raud","year":"2019","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reasoning 62(3), 331\u2013365 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9431-7","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"2_CR44","first-page":"237","volume":"11","author":"JC Chen","year":"2003","unstructured":"Chen, J.C.: Dijkstra\u2019s shortest path algorithm. Formalized Mathematics 11(3), 237\u2013247 (2003). \nhttp:\/\/fm.mizar.org\/2003-11\/pdf11-3\/graphsp.pdf","journal-title":"Formalized Mathematics"},{"key":"2_CR45","unstructured":"Chen, R., Cohen, C., L\u00e9vy, J., Merz, S., Th\u00e9ry, L.: Formal proofs of Tarjan\u2019s strongly connected components algorithm in Why3, Coq and Isabelle. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019. LIPIcs, vol. 141, pp. 13:1\u201313:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.13"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Chen, R., L\u00e9vy, J.: A semi-automatic proof of strong connectivity. In: Paskevich and Wies [160], pp. 49\u201365. \nhttps:\/\/doi.org\/10.1007\/978-3-319-72308-2_4","DOI":"10.1007\/978-3-319-72308-2_4"},{"key":"2_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-12154-3_11","volume-title":"Verified Software: Theories, Tools and Experiments","author":"M Clochard","year":"2014","unstructured":"Clochard, M.: Automatically verified implementation of data structures based on AVL trees. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 167\u2013180. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-12154-3_11"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Conchon, S., Filli\u00e2tre, J.: A persistent union-find data structure. In: Russo, C.V., Dreyer, D. (eds.) Workshop on ML, 2007. pp. 37\u201346. ACM (2007). \nhttps:\/\/doi.org\/10.1145\/1292535.1292541","DOI":"10.1145\/1292535.1292541"},{"key":"2_CR49","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd Edition. MIT Press (2009). \nhttp:\/\/mitpress.mit.edu\/books\/introduction-algorithms"},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008. pp. 133\u2013144. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1328438.1328457","DOI":"10.1145\/1328438.1328457"},{"key":"2_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-32347-8_7","volume-title":"Interactive Theorem Proving","author":"M D\u00e9n\u00e8s","year":"2012","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 83\u201398. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_7"},{"key":"2_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-57288-8_5","volume-title":"NASA Formal Methods","author":"C Dross","year":"2017","unstructured":"Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 68\u201383. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-57288-8_5"},{"key":"2_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-14052-5_16","volume-title":"Interactive Theorem Proving","author":"J-F Dufourd","year":"2010","unstructured":"Dufourd, J.-F., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 211\u2013226. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14052-5_16"},{"key":"2_CR54","unstructured":"Eberl, M.: Fisher-yates shuffle. Archive of Formal Proofs, September 2016. \nhttp:\/\/isa-afp.org\/entries\/Fisher_Yates.html\n\n, Formal proof development"},{"key":"2_CR55","unstructured":"Eberl, M.: Expected shape of random binary search trees. Archive of Formal Proofs, April 2017. \nhttp:\/\/isa-afp.org\/entries\/Random_BSTs.html\n\n, Formal proof development"},{"key":"2_CR56","unstructured":"Eberl, M.: Lower bound on comparison-based sorting algorithms. Archive of Formal Proofs, March 2017. \nhttp:\/\/isa-afp.org\/entries\/Comparison_Sort_Lower_Bound.html\n\n, Formal proof development"},{"key":"2_CR57","unstructured":"Eberl, M.: The median-of-medians selection algorithm. Archive of Formal Proofs, December 2017. \nhttp:\/\/isa-afp.org\/entries\/Median_Of_Medians_Selection.html\n\n, Formal proof development"},{"key":"2_CR58","unstructured":"Eberl, M.: The number of comparisons in quicksort. Archive of Formal Proofs, March 2017. \nhttp:\/\/isa-afp.org\/entries\/Quick_Sort_Cost.html\n\n, Formal proof development"},{"issue":"4","key":"2_CR59","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-016-9378-0","volume":"58","author":"M Eberl","year":"2017","unstructured":"Eberl, M.: Proving divide and conquer complexities in Isabelle\/HOL. J. Autom. Reasoning 58(4), 483\u2013508 (2017). \nhttps:\/\/doi.org\/10.1007\/s10817-016-9378-0","journal-title":"J. Autom. Reasoning"},{"key":"2_CR60","doi-asserted-by":"publisher","unstructured":"Eberl, M.: Verified real asymptotics in Isabelle\/HOL. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation. ISSAC 2019. ACM, New York (2019). \nhttps:\/\/doi.org\/10.1145\/3326229.3326240","DOI":"10.1145\/3326229.3326240"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. In: J. Automated Reasoning (2020). \nhttps:\/\/doi.org\/10.1007\/s10817-020-09545-0","DOI":"10.1007\/s10817-020-09545-0"},{"key":"2_CR62","doi-asserted-by":"publisher","first-page":"44","DOI":"10.4153\/CJM-1965-045-4","volume":"17","author":"J Edmonds","year":"1965","unstructured":"Edmonds, J.: Paths, trees, and flowers. Can. J. Math. 17, 44\u2013467 (1965). \nhttps:\/\/doi.org\/10.4153\/CJM-1965-045-4","journal-title":"Can. J. Math."},{"issue":"6","key":"2_CR63","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and verifythis competition. Int. J. Softw. Tools Technol. Transf. 17(6), 677\u2013694 (2015). \nhttps:\/\/doi.org\/10.1007\/s10009-014-0308-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"2_CR64","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s10270-013-0320-1","volume":"14","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Schellhorn, G., Reif, W.: Verification of B$$^{\\text{+ }}$$ trees by integration of shape analysis and interactive theorem proving. Software Syst. Model. 14(1), 27\u201344 (2015). \nhttps:\/\/doi.org\/10.1007\/s10270-013-0320-1","journal-title":"Software Syst. Model."},{"key":"2_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"key":"2_CR66","doi-asserted-by":"crossref","unstructured":"E\u00dfmann, R., Nipkow, T., Robillard, S.: Verified approximation algorithms. In: Peltier and Sofronie-Stokkermans [163], pp. 291\u2013306. \nhttps:\/\/doi.org\/10.1007\/978-3-030-51054-1_17","DOI":"10.1007\/978-3-030-51054-1_17"},{"key":"2_CR67","unstructured":"Filli\u00e2tre, J.C.: Knuth-Morris-Pratt string searching algorithm. \nhttp:\/\/toccata.lri.fr\/gallery\/kmp.en.html\n\n, formal proof development"},{"key":"2_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-48167-2_6","volume-title":"Types for Proofs and Programs","author":"J-C Filli\u00e2tre","year":"1999","unstructured":"Filli\u00e2tre, J.-C.: Proof of imperative programs in type theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 78\u201392. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48167-2_6"},{"key":"2_CR69","unstructured":"Filli\u00e2tre, J.C.: Skew heaps (2014). \nhttp:\/\/toccata.lri.fr\/gallery\/skew_heaps.en.html\n\n, formal proof development"},{"key":"2_CR70","unstructured":"Filli\u00e2tre, J.C.: Purely applicative heaps implemented with Braun trees (2015). \nhttp:\/\/toccata.lri.fr\/gallery\/braun_trees.en.html\n\n, formal proof development"},{"key":"2_CR71","unstructured":"Filli\u00e2tre, J.C.: Binomial heaps (2016). \nhttp:\/\/toccata.lri.fr\/gallery\/binomial_heap.en.html\n\n, formal proof development"},{"key":"2_CR72","unstructured":"Filli\u00e2tre, J.C., Clochard, M.: Hash tables with linear probing (2014). \nhttp:\/\/toccata.lri.fr\/gallery\/linear_probing.en.html\n\n, formal proof development"},{"key":"2_CR73","unstructured":"Filli\u00e2tre, J.C., Clochard, M.: Warshall algorithm (2014), \nhttp:\/\/toccata.lri.fr\/gallery\/warshall_algorithm.en.html\n\n, formal proof development"},{"key":"2_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 370\u2013384. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24725-8_26"},{"key":"2_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"2_CR76","unstructured":"Filli\u00e2tre, J., Paskevich, A., Stump, A.: The 2nd verified software competition: Experience report. In: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, pp. 36\u201349 (2012). \nhttp:\/\/ceur-ws.org\/Vol-873\/papers\/paper_6.pdf"},{"issue":"1","key":"2_CR77","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BF01840439","volume":"1","author":"ML Fredman","year":"1986","unstructured":"Fredman, M.L., Sedgewick, R., Sleator, D.D., Tarjan, R.E.: The pairing heap: a new form of self-adjusting heap. Algorithmica 1(1), 111\u2013129 (1986). \nhttps:\/\/doi.org\/10.1007\/BF01840439","journal-title":"Algorithmica"},{"issue":"6","key":"2_CR78","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/s10009-016-0419-0","volume":"19","author":"CA Furia","year":"2017","unstructured":"Furia, C.A., Nordio, M., Polikarpova, N., Tschannen, J.: Autoproof: auto-active functional verification of object-oriented programs. Int. J. Softw. Tools Technol. Transf. 19(6), 697\u2013716 (2017). \nhttps:\/\/doi.org\/10.1007\/s10009-016-0419-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3\u20134","key":"2_CR79","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0020-0190(00)00051-X","volume":"74","author":"HN Gabow","year":"2000","unstructured":"Gabow, H.N.: Path-based depth-first search for strong and biconnected components. Inf. Process. Lett. 74(3\u20134), 107\u2013114 (2000). \nhttps:\/\/doi.org\/10.1016\/S0020-0190(00)00051-X","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"2_CR80","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1080\/00029890.1962.11989827","volume":"69","author":"D Gale","year":"1962","unstructured":"Gale, D., Shapley, L.S.: College admissions and the stability of marriage. Am. Math. Monthly 69(1), 9\u201315 (1962)","journal-title":"Am. Math. Monthly"},{"key":"2_CR81","unstructured":"Galperin, I., Rivest, R.L.: Scapegoat trees. In: Ramachandran, V. (ed.) Proceedings of the Fourth Annual ACM\/SIGACT-SIAM Symposium on Discrete Algorithms, pp. 165\u2013174. ACM\/SIAM (1993). \nhttp:\/\/dl.acm.org\/citation.cfm?id=313559.313676"},{"issue":"1","key":"2_CR82","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1012912614285","volume":"20","author":"R Gamboa","year":"2002","unstructured":"Gamboa, R.: The correctness of the fast Fourier transform: a structured proof in ACL2. Formal Methods Syst. Des. 20(1), 91\u2013106 (2002)","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"2_CR84","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical Aspects of Topology and Analysis","author":"M Giry","year":"1982","unstructured":"Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68\u201385. Springer, Heidelberg (1982). \nhttps:\/\/doi.org\/10.1007\/BFb0092872"},{"issue":"1","key":"2_CR85","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10817-017-9426-4","volume":"62","author":"S de Gouw","year":"2019","unstructured":"de Gouw, S., de Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. J. Autom. Reasoning 62(1), 93\u2013126 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9426-4","journal-title":"J. Autom. Reasoning"},{"key":"2_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S de Gouw","year":"2015","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_16"},{"key":"2_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-319-89884-1_19","volume-title":"Programming Languages and Systems","author":"A Gu\u00e9neau","year":"2018","unstructured":"Gu\u00e9neau, A., Chargu\u00e9raud, A., Pottier, F.: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 533\u2013560. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89884-1_19"},{"key":"2_CR88","doi-asserted-by":"crossref","unstructured":"Guibas, L.J., McCreight, E.M., Plass, M.F., Roberts, J.R.: A new representation for linear lists. In: Hopcroft, J.E., Friedman, E.P., Harrison, M.A. (eds.) Proceedings of the 9th Annual ACM Symposium on Theory of Computing, pp. 49\u201360. ACM (1977). \nhttps:\/\/doi.org\/10.1145\/800105.803395","DOI":"10.1145\/800105.803395"},{"key":"2_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-46750-4_4","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"W Guttmann","year":"2016","unstructured":"Guttmann, W.: Relation-algebraic verification of Prim\u2019s minimum spanning tree algorithm. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 51\u201368. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-46750-4_4"},{"key":"2_CR90","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.tcs.2018.04.012","volume":"744","author":"W Guttmann","year":"2018","unstructured":"Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theor. Comput. Sci. 744, 37\u201355 (2018). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2018.04.012","journal-title":"Theor. Comput. Sci."},{"key":"2_CR91","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1016\/j.jlamp.2018.09.005","volume":"101","author":"W Guttmann","year":"2018","unstructured":"Guttmann, W.: Verifying minimum spanning tree algorithms with stone relation algebras. J. Log. Algebraic Methods Program 101, 132\u2013150 (2018). \nhttps:\/\/doi.org\/10.1016\/j.jlamp.2018.09.005","journal-title":"J. Log. Algebraic Methods Program"},{"key":"2_CR92","doi-asserted-by":"crossref","unstructured":"Hamid, N.A., Castleberry, C.: Formally certified stable marriages. In: Proceedings of the 48th Annual Southeast Regional Conference. ACM SE 2010. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1900008.1900056","DOI":"10.1145\/1900008.1900056"},{"key":"2_CR93","unstructured":"Haslbeck, M.W., Eberl, M.: Skip lists. Archive of Formal Proofs, January 2020. \nhttp:\/\/isa-afp.org\/entries\/Skip_Lists.html\n\n, Formal proof development"},{"key":"2_CR94","unstructured":"Haslbeck, M.W., Eberl, M., Nipkow, T.: Treaps. Archive of Formal Proofs, February 2018. \nhttp:\/\/isa-afp.org\/entries\/Treaps.html\n\n, Formal proof development"},{"key":"2_CR95","unstructured":"Haslbeck, M.P.L., Lammich, P.: Refinement with time \u2013 refining the run-time of algorithms in Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) Interactive Theorem Proving, ITP 2019. LIPIcs, vol. 141, pp. 20:1\u201320:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.20"},{"key":"2_CR96","unstructured":"Haslbeck, M.P.L., Lammich, P., Biendarra, J.: Kruskal\u2019s algorithm for minimum spanning forest. Archive of Formal Proofs, February 2019. \nhttp:\/\/isa-afp.org\/entries\/Kruskal.html\n\n, Formal proof development"},{"key":"2_CR97","unstructured":"Haslbeck, M.P.L., Lammich, P., Biendarra, J.: Kruskal\u2019s algorithm for minimum spanning forest. Arch. Formal Proofs 2019 (2019), \nhttps:\/\/www.isa-afp.org\/entries\/Kruskal.html"},{"key":"2_CR98","doi-asserted-by":"publisher","unstructured":"Haslbeck, M.P.L., Nipkow, T.: Verified analysis of list update algorithms. In: Lal, A., Akshay, S., Saurabh, S., Sen, S. (eds.) Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. LIPIcs, vol. 65, pp. 49:1\u201349:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2016.49\n\n, \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2016.49","DOI":"10.4230\/LIPIcs.FSTTCS.2016.49"},{"key":"2_CR99","unstructured":"Hellauer, F., Lammich, P.: The string search algorithm by knuth, morris and pratt. Archive of Formal Proofs, December 2017. \nhttp:\/\/isa-afp.org\/entries\/Knuth_Morris_Pratt.html\n\n, Formal proof development"},{"key":"2_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-45237-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-DA Hiep","year":"2020","unstructured":"Hiep, H.-D.A., Maathuis, O., Bian, J., de Boer, F.S., van Eekelen, M., de Gouw, S.: Verifying OpenJDK\u2019s LinkedList using KeY. TACAS 2020. LNCS, vol. 12079, pp. 217\u2013234. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45237-7_13"},{"issue":"2","key":"2_CR101","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1017\/S0956796805005769","volume":"16","author":"R Hinze","year":"2006","unstructured":"Hinze, R., Paterson, R.: Finger trees: a simple general-purpose data structure. J. Funct. Program. 16(2), 197\u2013217 (2006). \nhttps:\/\/doi.org\/10.1017\/S0956796805005769","journal-title":"J. Funct. Program."},{"issue":"3","key":"2_CR102","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S0956796811000104","volume":"21","author":"Y Hirai","year":"2011","unstructured":"Hirai, Y., Yamamoto, K.: Balancing weight-balanced trees. J. Funct. Program. 21(3), 287\u2013307 (2011). \nhttps:\/\/doi.org\/10.1017\/S0956796811000104","journal-title":"J. Funct. Program."},{"key":"2_CR103","unstructured":"Hoffmann, J.: Types with potential: polynomial resource bounds via automatic amortized analysis. Ph.D. thesis, Ludwig Maximilians University Munich (2011). \nhttp:\/\/edoc.ub.uni-muenchen.de\/13955\/"},{"key":"2_CR104","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012). \nhttps:\/\/doi.org\/10.1145\/2362389.2362393","DOI":"10.1145\/2362389.2362393"},{"key":"2_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-319-43144-4_30","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2016","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 475\u2013482. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-43144-4_30"},{"key":"2_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22863-6_12"},{"key":"2_CR107","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279\u2013294. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_21"},{"key":"2_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-56625-2_14","volume-title":"Mathematics of Program Construction","author":"RR Hoogerwoord","year":"1993","unstructured":"Hoogerwoord, R.R.: A logarithmic implementation of flexible arrays. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds.) MPC 1992. LNCS, vol. 669, pp. 191\u2013207. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/3-540-56625-2_14"},{"issue":"1\u20132","key":"2_CR109","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S1567-8326(02)00065-6","volume":"56","author":"J Hurd","year":"2003","unstructured":"Hurd, J.: Verification of the Miller-Rabin probabilistic primality test. J. Log. Algebraic Methods Program. 56(1\u20132), 3\u201321 (2003). \nhttps:\/\/doi.org\/10.1016\/S1567-8326(02)00065-6","journal-title":"J. Log. Algebraic Methods Program."},{"key":"2_CR110","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"key":"2_CR111","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"2_CR112","unstructured":"Keinholz, J.: Matroids. Archive of Formal Proofs, November 2018. \nhttp:\/\/isa-afp.org\/entries\/Matroids.html\n\n, Formal proof development"},{"key":"2_CR113","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/BF00264289","volume":"1","author":"DE Knuth","year":"1971","unstructured":"Knuth, D.E.: Optimum binary search trees. Acta Inf. 1, 14\u201325 (1971). \nhttps:\/\/doi.org\/10.1007\/BF00264289","journal-title":"Acta Inf."},{"key":"2_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84\u201399. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_9"},{"key":"2_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-08970-6_21","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2014","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325\u2013340. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08970-6_21"},{"key":"2_CR116","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: Urban and Zhang [191], pp. 253\u2013269. \nhttps:\/\/doi.org\/10.1007\/978-3-319-22102-1_17","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"2_CR117","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 27\u201336. ACM (2016). \nhttps:\/\/doi.org\/10.1145\/2854065.2854067","DOI":"10.1145\/2854065.2854067"},{"key":"2_CR118","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) Interactive Theorem Proving, ITP 2019. LIPIcs, vol. 141, pp. 22:1\u201322:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22"},{"issue":"4","key":"2_CR119","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to imperative HOL. J. Autom. Reasoning 62(4), 481\u2013503 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9437-1","journal-title":"J. Autom. Reasoning"},{"key":"2_CR120","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-030-51054-1_18","volume-title":"Automated Reasoning","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified implementation of Introsort and Pdqsort. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 307\u2013323. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-51054-1_18"},{"key":"2_CR121","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339\u2013354. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14052-5_24"},{"key":"2_CR122","unstructured":"Lammich, P., Meis, R.: A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs, November 2012. \nhttp:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html\n\n, Formal proof development"},{"key":"2_CR123","doi-asserted-by":"crossref","unstructured":"Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: Leroy, X., Tiu, A. (eds.) Proceedings of the 2015 Conference on Certified Programs and Proofs. CPP 2015, pp. 137\u2013146. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2676724.2693165","DOI":"10.1145\/2676724.2693165"},{"key":"2_CR124","unstructured":"Lammich, P., Nipkow, T.: Proof pearl: purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) Interactive Theorem Proving, ITP 2019. LIPIcs, vol. 141, pp. 23:1\u201323:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.23"},{"key":"2_CR125","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-43144-4_14","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2016","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 219\u2013234. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-43144-4_14"},{"issue":"2","key":"2_CR126","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-017-9442-4","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing network flow algorithms: a refinement approach in Isabelle\/HOL. J. Autom. Reasoning 62(2), 261\u2013280 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9442-4","journal-title":"J. Autom. Reasoning"},{"key":"2_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"2_CR128","unstructured":"Lee, G.: Correctnesss of Ford-Fulkerson\u2019s maximum flow algorithm. Formalized Math. 13(2), 305\u2013314 (2005). \nhttp:\/\/fm.mizar.org\/2005-13\/pdf13-2\/glib_005.pdf"},{"key":"2_CR129","unstructured":"Lee, G., Rudnicki, P.: Correctness of Dijkstra\u2019s shortest path and Prim\u2019s minimum spanning tree algorithms. Formal. Math. 13(2), 295\u2013304 (2005). \nhttp:\/\/fm.mizar.org\/2005-13\/pdf13-2\/glib_004.pdf"},{"key":"2_CR130","unstructured":"Leighton, T.: Notes on better master theorems for divide-and-conquer recurrences (MIT lecture notes) (1996), \nhttps:\/\/courses.csail.mit.edu\/6.046\/spring04\/handouts\/akrabazzi.pdf"},{"key":"2_CR131","doi-asserted-by":"crossref","unstructured":"Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 237\u2013248. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1706299.1706329","DOI":"10.1145\/1706299.1706329"},{"key":"2_CR132","unstructured":"Mari\u0107, F., Spasi\u0107, M., Thiemann, R.: An incremental simplex algorithm with unsatisfiable core generation. Archive of Formal Proofs, August 2018. \nhttp:\/\/isa-afp.org\/entries\/Simplex.html\n\n, Formal proof development"},{"key":"2_CR133","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-29604-3_10","volume-title":"Functional and Logic Programming","author":"J McCarthy","year":"2016","unstructured":"McCarthy, J., Fetscher, B., New, M., Feltey, D., Findler, R.B.: A coq library for internal verification of running-times. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 144\u2013162. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-29604-3_10"},{"key":"2_CR134","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry","author":"LI Meikle","year":"2006","unstructured":"Meikle, L.I., Fleuriot, J.D.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 1\u201318. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11615798_1"},{"key":"2_CR135","unstructured":"Meis, R., Nielsen, F., Lammich, P.: Binomial heaps and skew binomial heaps. Archive of Formal Proofs, October 2010. \nhttp:\/\/isa-afp.org\/entries\/Binomial-Heaps.html\n\n, Formal proof development"},{"key":"2_CR136","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall (1991). \nhttp:\/\/www.eiffel.com\/doc\/#etl"},{"key":"2_CR137","unstructured":"Moore, J S., Martinez, M.: A mechanically checked proof of the correctness of the Boyer-Moore fast string searching algorithm. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, pp. 267\u2013284. IOS Press (2009)"},{"key":"2_CR138","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/11541868_24","volume-title":"Theorem Proving in Higher Order Logics","author":"JS Moore","year":"2005","unstructured":"Moore, J.S., Zhang, Q.: Proof pearl: Dijkstra\u2019s shortest path algorithm verified with ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 373\u2013384. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11541868_24"},{"key":"2_CR139","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"2_CR140","unstructured":"Musser, D.R.: Introspective sorting and selection algorithms. Softw. Pract. Exp. 27(8), 983\u2013993 (1997). \nhttps:\/\/doi.org\/10.1002\/(SICI)1097--024X(199708)27:8<983::AID-SPE117>3.0.CO;2-%23"},{"key":"2_CR141","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008. pp. 229\u2013240. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1411204.1411237","DOI":"10.1145\/1411204.1411237"},{"key":"2_CR142","unstructured":"Neumann, R.: CAVA \u2013 A Verified Model Checker. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2017). \nhttp:\/\/nbn-resolving.de\/urn\/resolver.pl?urn:nbn:de:bvb:91-diss-20170616-1342881-1-9"},{"key":"2_CR143","doi-asserted-by":"crossref","unstructured":"Nievergelt, J., Reingold, E.M.: Binary search trees of bounded balance. In: Fischer, P.C., Zeiger, H.P., Ullman, J.D., Rosenberg, A.L. (eds.) Proceedings of the 4th Annual ACM Symposium on Theory of Computing, pp. 137\u2013142. ACM (1972). \nhttps:\/\/doi.org\/10.1145\/800152.804906","DOI":"10.1145\/800152.804906"},{"issue":"1","key":"2_CR144","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1137\/0202005","volume":"2","author":"J Nievergelt","year":"1973","unstructured":"Nievergelt, J., Reingold, E.M.: Binary search trees of bounded balance. SIAM J. Comput. 2(1), 33\u201343 (1973). \nhttps:\/\/doi.org\/10.1137\/0202005","journal-title":"SIAM J. Comput."},{"key":"2_CR145","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Amortized complexity verified. In: Urban and Zhang [191], pp. 310\u2013324. \nhttps:\/\/doi.org\/10.1007\/978-3-319-22102-1_21","DOI":"10.1007\/978-3-319-22102-1_21"},{"key":"2_CR146","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-43144-4_19","volume-title":"Interactive Theorem Proving","author":"T Nipkow","year":"2016","unstructured":"Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 307\u2013322. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-43144-4_19"},{"key":"2_CR147","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Verified root-balanced trees. In: Chang, B.E. (ed.) Programming Languages and Systems, APLAS 2017. LNCS, vol. 10695, pp. 255\u2013272. Springer (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-71237-6_13","DOI":"10.1007\/978-3-319-71237-6_13"},{"issue":"3","key":"2_CR148","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9459-3","volume":"62","author":"T Nipkow","year":"2019","unstructured":"Nipkow, T., Brinkop, H.: Amortized complexity verified. J. Autom. Reasoning 62(3), 367\u2013391 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-018-9459-3","journal-title":"J. Autom. Reasoning"},{"key":"2_CR149","unstructured":"Nipkow, T., Dirix, S.: Weight-balanced trees. Archive of Formal Proofs, March 2018. \nhttp:\/\/isa-afp.org\/entries\/Weight_Balanced_Trees.html\n\n, Formal proof development"},{"key":"2_CR150","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle\/HOL. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10542-0\n\n, \nhttp:\/\/www.concrete-semantics.org\/","DOI":"10.1007\/978-3-319-10542-0"},{"key":"2_CR151","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"2_CR152","unstructured":"Nipkow, T., Pusch, C.: AVL trees. Archive of Formal Proofs, March 2004. \nhttp:\/\/isa-afp.org\/entries\/AVL-Trees.html\n\n, Formal proof development"},{"key":"2_CR153","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Sewell, T.: Proof pearl: Braun trees. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 18\u201331. ACM (2020). \nhttps:\/\/doi.org\/10.1145\/3372885.3373834","DOI":"10.1145\/3372885.3373834"},{"key":"2_CR154","unstructured":"Nipkow, T., Somogyi, D.: Optimal binary search trees. Archive of Formal Proofs, May 2018. \nhttp:\/\/isa-afp.org\/entries\/Optimal_BST.html\n\n, Formal proof development"},{"key":"2_CR155","unstructured":"Nordhoff, B., K\u00f6rner, S., Lammich, P.: Finger trees. Archive of Formal Proofs, October 2010. \nhttp:\/\/isa-afp.org\/entries\/Finger-Trees.html\n\n, Formal proof development"},{"key":"2_CR156","unstructured":"Nordhoff, B., Lammich, P.: Dijkstra\u2019s shortest path algorithm. Archive of Formal Proofs, January 2012. \nhttp:\/\/isa-afp.org\/entries\/Dijkstra_Shortest_Path.html\n\n, Formal proof development"},{"key":"2_CR157","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-71067-7_5","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owre","year":"2008","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 22\u201327. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_5"},{"key":"2_CR158","unstructured":"Palomo-Lozano, F., Inmaculada Medina-Bulo, J.A.A.J.: Certification of matrix multiplication algorithms. In: Theorem Proving in Higher Order Logics, Supplemental Proceedings, TPHOLs 2001 (2001)"},{"key":"2_CR159","unstructured":"Parsert, J., Kaliszyk, C.: Linear programming. Archive of Formal Proofs, August 2019. \nhttp:\/\/isa-afp.org\/entries\/Linear_Programming.html\n\n, Formal proof development"},{"key":"2_CR160","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72308-2","volume-title":"Verified Software. Theories, Tools, and Experiments","year":"2017","unstructured":"Paskevich, A., Wies, T. (eds.): VSTTE 2017. LNCS, vol. 10712. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-72308-2"},{"key":"2_CR161","unstructured":"Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions). Ph.D. thesis, Paris Diderot University, France (1989). \nhttps:\/\/tel.archives-ouvertes.fr\/tel-00431825"},{"key":"2_CR162","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"LC Paulson","year":"1996","unstructured":"Paulson, L.C.: ML for the Working Programmer, 2nd edn. Cambridge University Press, Cambridge (1996)","edition":"2"},{"key":"2_CR163","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1","volume-title":"Automated Reasoning","year":"2020","unstructured":"Peltier, N., Sofronie-Stokkermans, V. (eds.): IJCAR 2020. LNCS (LNAI), vol. 12167. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-51054-1"},{"key":"2_CR164","unstructured":"Pereira, M.: Pairing heaps (2016). \nhttp:\/\/toccata.lri.fr\/gallery\/pairing_heap.en.html\n\n, formal proof development"},{"key":"2_CR165","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-662-46666-7_4","volume-title":"Principles of Security and Trust","author":"A Petcher","year":"2015","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53\u201372. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46666-7_4"},{"key":"2_CR166","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"Theorem Proving in Higher Order Logics","author":"D Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346\u2013361. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44755-5_24"},{"key":"2_CR167","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-319-19249-9_26","volume-title":"FM 2015: Formal Methods","author":"N Polikarpova","year":"2015","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 414\u2013434. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_26"},{"issue":"5","key":"2_CR168","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s00165-017-0435-1","volume":"30","author":"N Polikarpova","year":"2018","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. Formal Asp. Comput. 30(5), 495\u2013523 (2018). \nhttps:\/\/doi.org\/10.1007\/s00165-017-0435-1","journal-title":"Formal Asp. Comput."},{"key":"2_CR169","unstructured":"Pottier, F.: Depth-first search and strong connectivity in Coq. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA), January 2015. \nhttp:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-dfs-scc.pdf"},{"key":"2_CR170","doi-asserted-by":"publisher","unstructured":"Pottier, F.: Verifying a hash table and its iterators in higher-order separation logic. In: ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pp. 3\u201316, January 2017. \nhttps:\/\/doi.org\/10.1145\/3018610.3018624\n\n, \nhttp:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-hashtable.pdf","DOI":"10.1145\/3018610.3018624"},{"issue":"6","key":"2_CR171","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: a probabilistic alternative to balanced trees. Commun. ACM 33(6), 668\u2013676 (1990). \nhttps:\/\/doi.org\/10.1145\/78973.78977","journal-title":"Commun. ACM"},{"key":"2_CR172","doi-asserted-by":"crossref","unstructured":"Ralston, R.: ACL2-certified AVL trees. In: Eighth International Workshop on the ACL2 Theorem Prover and Its Applications. ACL2 2009, pp. 71\u201374. ACM (2009). \nhttps:\/\/doi.org\/10.1145\/1637837.1637848","DOI":"10.1145\/1637837.1637848"},{"key":"2_CR173","doi-asserted-by":"crossref","unstructured":"Rau, M., Nipkow, T.: Verification of closest pair of points algorithms. In: Peltier and Sofronie-Stokkermans [163], pp. 341\u2013357. \nhttps:\/\/doi.org\/10.1007\/978-3-030-51054-1_20","DOI":"10.1007\/978-3-030-51054-1_20"},{"key":"2_CR174","unstructured":"Rem, M., Braun, W.: A logarithmic implementation of flexible arrays (1983). memorandum MR83\/4. Eindhoven University of Technology"},{"issue":"3","key":"2_CR175","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002). \nhttps:\/\/doi.org\/10.1145\/514188.514190","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR176","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-90686-7_4","volume-title":"Functional and Logic Programming","author":"K Sakaguchi","year":"2018","unstructured":"Sakaguchi, K.: Program extraction for mutable arrays. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 51\u201367. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-90686-7_4"},{"key":"2_CR177","unstructured":"Sedgewick, R., Wayne, K.: Algorithms, 4th Edition. Addison-Wesley, Upper Saddle River (2011)"},{"issue":"4\/5","key":"2_CR178","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BF01940876","volume":"16","author":"R Seidel","year":"1996","unstructured":"Seidel, R., Aragon, C.R.: Randomized search trees. Algorithmica 16(4\/5), 464\u2013497 (1996). \nhttps:\/\/doi.org\/10.1007\/BF01940876","journal-title":"Algorithmica"},{"issue":"3","key":"2_CR179","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1145\/3828.3835","volume":"32","author":"DD Sleator","year":"1985","unstructured":"Sleator, D.D., Tarjan, R.E.: Self-adjusting binary search trees. J. ACM 32(3), 652\u2013686 (1985). \nhttps:\/\/doi.org\/10.1145\/3828.3835","journal-title":"J. ACM"},{"issue":"1","key":"2_CR180","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1137\/0215004","volume":"15","author":"DD Sleator","year":"1986","unstructured":"Sleator, D.D., Tarjan, R.E.: Self-adjusting heaps. SIAM J. Comput. 15(1), 52\u201369 (1986). \nhttps:\/\/doi.org\/10.1137\/0215004","journal-title":"SIAM J. Comput."},{"key":"2_CR181","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"2_CR182","doi-asserted-by":"crossref","unstructured":"Sozeau, M.: Program-ing finger trees in Coq. In: Hinze, R., Ramsey, N. (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming. ICFP 2007, pp. 13\u201324. ACM (2007). \nhttps:\/\/doi.org\/10.1145\/1291220.1291156","DOI":"10.1145\/1291220.1291156"},{"key":"2_CR183","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-32759-9_35","volume-title":"FM 2012: Formal Methods","author":"M Spasi\u0107","year":"2012","unstructured":"Spasi\u0107, M., Mari\u0107, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 434\u2013449. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_35"},{"key":"2_CR184","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-319-57418-9_18","volume-title":"Relational and Algebraic Methods in Computer Science","author":"I Stucke","year":"2017","unstructured":"Stucke, I.: Reasoning about cardinalities of relations with applications supported by proof assistants. In: H\u00f6fner, P., Pous, D., Struth, G. (eds.) RAMICS 2017. LNCS, vol. 10226, pp. 290\u2013306. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-57418-9_18"},{"key":"2_CR185","unstructured":"St\u00fcwe, D., Eberl, M.: Probabilistic primality testing. Archive of Formal Proofs, February 2019. \nhttp:\/\/isa-afp.org\/entries\/Probabilistic_Prime_Tests.html\n\n, Formal proof development"},{"issue":"2","key":"2_CR186","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). \nhttps:\/\/doi.org\/10.1137\/0201010","journal-title":"SIAM J. Comput."},{"key":"2_CR187","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/978-3-319-94821-8_33","volume-title":"Interactive Theorem Proving","author":"J Tassarotti","year":"2018","unstructured":"Tassarotti, J., Harper, R.: Verified tail bounds for randomized programs. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 560\u2013578. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-94821-8_33"},{"key":"2_CR188","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Harper, R.: A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL), 64:1\u201364:30 (2019). \nhttps:\/\/doi.org\/10.1145\/3290377","DOI":"10.1145\/3290377"},{"key":"2_CR189","unstructured":"Th\u00e9ry, L.: Formalising Huffman\u2019s algorithm. Research report, Universit\u00e0 degli Studi dell\u2019Aquila (2004) \nhttps:\/\/hal.archives-ouvertes.fr\/hal-02149909"},{"key":"2_CR190","unstructured":"Toibazarov, E.: An ACL2 proof of the correctness of the preprocessing for a variant of the Boyer-Moore fast string searching algorithm. Honors thesis, Computer Science Dept., University of Texas at Austin (2013). see \nwww.cs.utexas.edu\/users\/moore\/publications\/toibazarov-thesis.pdf"},{"key":"2_CR191","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1","volume-title":"Interactive Theorem Proving","year":"2015","unstructured":"Urban, C., Zhang, X. (eds.): ITP 2015. LNCS, vol. 9236. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-22102-1"},{"key":"2_CR192","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-39634-2_24","volume-title":"Interactive Theorem Proving","author":"V Vafeiadis","year":"2013","unstructured":"Vafeiadis, V.: Adjustable references. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 328\u2013337. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_24"},{"key":"2_CR193","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-02444-3_16","volume-title":"Types for Proofs and Programs","author":"E van der Weegen","year":"2009","unstructured":"van der Weegen, E., McKinna, J.: A machine-checked proof of the average-case complexity of quicksort in Coq. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 256\u2013271. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02444-3_16"},{"key":"2_CR194","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-319-43144-4_26","volume-title":"Interactive Theorem Proving","author":"S Wimmer","year":"2016","unstructured":"Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 425\u2013440. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-43144-4_26"},{"key":"2_CR195","unstructured":"Wimmer, S.: Hidden Markov models. Archive of Formal Proofs, May 2018. \nhttp:\/\/isa-afp.org\/entries\/Hidden_Markov_Models.html\n\n, Formal proof development"},{"key":"2_CR196","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-319-94821-8_34","volume-title":"Interactive Theorem Proving","author":"S Wimmer","year":"2018","unstructured":"Wimmer, S., Hu, S., Nipkow, T.: Verified Memoization and dynamic programming. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 579\u2013596. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-94821-8_34"},{"key":"2_CR197","unstructured":"Wimmer, S., Lammich, P.: The Floyd-Warshall algorithm for shortest paths. Archive of Formal Proofs, May 2017. \nhttp:\/\/isa-afp.org\/entries\/Floyd_Warshall.html\n\n, Formal proof development"},{"key":"2_CR198","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-89960-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Wimmer","year":"2018","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61\u201378. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89960-2_4"},{"key":"2_CR199","doi-asserted-by":"crossref","unstructured":"Yao, F.F.: Efficient dynamic programming using quadrangle inequalities. In: Miller, R.E., Ginsburg, S., Burkhard, W.A., Lipton, R.J. (eds.) Proceedings of the 12th Annual ACM Symposium on Theory of Computing, pp. 429\u2013435. ACM (1980). \nhttps:\/\/doi.org\/10.1145\/800141.804691","DOI":"10.1145\/800141.804691"},{"key":"2_CR200","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-89960-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Zhan","year":"2018","unstructured":"Zhan, B.: Efficient verification of imperative programs using Auto2. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 23\u201340. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89960-2_2"},{"key":"2_CR201","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-319-94205-6_35","volume-title":"Automated Reasoning","author":"B Zhan","year":"2018","unstructured":"Zhan, B., Haslbeck, M.P.L.: Verifying asymptotic time complexity of\u00a0imperative programs in Isabelle. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 532\u2013548. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-94205-6_35"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59152-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:03:56Z","timestamp":1602457436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59152-6_2"}},"subtitle":["A Biased Survey"],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030591519","9783030591526"],"references-count":201,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hanoi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fit.uet.vnu.edu.vn\/atva2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}