{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:09:17Z","timestamp":1765667357487,"version":"3.40.3"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816872"},{"type":"electronic","value":"9783030816889"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We develop machine-checked verifications of the full functional correctness of C implementations of the eponymous graph algorithms of Dijkstra, Kruskal, and Prim. We extend Wang <jats:italic>et al.<\/jats:italic>\u2019s CertiGraph platform to reason about labels on edges, undirected graphs, and common spatial representations of edge-labeled graphs such as adjacency matrices and edge lists. We certify binary heaps, including Floyd\u2019s bottom-up heap construction, heapsort, and increase\/decrease priority.<\/jats:p><jats:p>Our verifications uncover subtle overflows implicit in standard textbook code, including a nontrivial bound on edge weights necessary to execute Dijkstra\u2019s algorithm; we show that the intuitive guess fails and provide a workable refinement. We observe that the common notion that Prim\u2019s algorithm requires a connected graph is wrong: we verify that a standard textbook implementation of Prim\u2019s algorithm can compute minimum spanning forests without finding components first. Our verification of Kruskal\u2019s algorithm reasons about two graphs simultaneously: the undirected graph undergoing MSF construction, and the directed graph representing the forest inside union-find. Our binary heap verification exposes precise bounds for the heap to operate correctly, avoids a subtle overflow error, and shows how to recycle keys to avoid overflow.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_37","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"801-826","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Functional Correctness of C Implementations of Dijkstra\u2019s, Kruskal\u2019s, and Prim\u2019s Algorithms"],"prefix":"10.1007","author":[{"given":"Anshuman","family":"Mohan","sequence":"first","affiliation":[]},{"given":"Wei Xiang","family":"Leow","sequence":"additional","affiliation":[]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"37_CR1","doi-asserted-by":"publisher","unstructured":"Functional Correctness of C implementations of Dijkstra\u2019s, Kruskal\u2019s, and Prim\u2019s Algorithms (2021). https:\/\/doi.org\/10.5281\/zenodo.4744664","DOI":"10.5281\/zenodo.4744664"},{"key":"37_CR2","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 (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"37_CR3","unstructured":"Anonymous: Prim\u2019s algorithm. https:\/\/en.wikipedia.org\/wiki\/Prim%27s_algorithm"},{"key":"37_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"37_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1093\/imamat\/15.2.161","volume":"15","author":"R Backhouse","year":"1975","unstructured":"Backhouse, R., Carr\u00e9, B.: Regular algebra applied to path-finding problems. J. Inst. Math. Appl. 15, 161\u2013186 (1975)","journal-title":"J. Inst. Math. Appl."},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_6"},{"key":"37_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9, 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"37_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"FM 2014: Formal Methods","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127\u2013131. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_9"},{"key":"37_CR10","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.: Local reasoning, separation and aliasing. In: SPACE (2004)"},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno, C., et al.: Moving fast with software verification. In: NASA Formal Methods Symposium (2015)","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: ICFP (2011)","DOI":"10.1145\/2034773.2034828"},{"key":"37_CR13","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.C., Pereira, M., Pottier, F.: VOCAL - a verified OCaml library. ML Family Workshop (2017)"},{"key":"37_CR14","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. Reason. 62, 331\u2013365 (2019)","journal-title":"J. Autom. Reason."},{"key":"37_CR15","unstructured":"Chen, J.C.: Dijkstra\u2019s shortest path algorithm. JFM 15, 237\u2013247 (2003)"},{"key":"37_CR16","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: ITP (2019)"},{"key":"37_CR17","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"WN Chin","year":"2010","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77, 1006\u20131036 (2010)","journal-title":"Sci. Comput. Program."},{"key":"37_CR18","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"Chou, C.T.: A formal theory of undirected graphs in HOL. In: HOL (1994)","DOI":"10.1007\/3-540-58450-1_40"},{"key":"37_CR20","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.S.: Introduction to Algorithms, 3rd edn. (2009)"},{"key":"37_CR21","unstructured":"Costa, D., Brotherston, J., Pym, D.: Graph decomposition and local reasoning (2020). Under submission"},{"key":"37_CR22","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1, 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"37_CR23","doi-asserted-by":"crossref","unstructured":"Dolan, S.: Fun with semirings: a functional pearl on the abuse of linear algebra. In: ICFP (2013)","DOI":"10.1145\/2500365.2500613"},{"key":"37_CR24","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. STTT 17, 677\u2013694 (2015)","journal-title":"STTT"},{"key":"37_CR25","unstructured":"Filli\u00e2tre, J.C.: Dijkstra\u2019s shortest path algorithm in Why3 (2011). http:\/\/toccata.lri.fr\/gallery\/dijkstra.en.html"},{"key":"37_CR26","doi-asserted-by":"crossref","unstructured":"Fillit\u0302re, J.C.: Simpler proofs with decentralized invariants. J. Log. Algebraic Methods Program. 121, 100645 (2021)","DOI":"10.1016\/j.jlamp.2021.100645"},{"issue":"12","key":"37_CR27","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/355588.365103","volume":"7","author":"RW Floyd","year":"1964","unstructured":"Floyd, R.W.: Algorithm 245: treesort. Commun. ACM 7(12), 701 (1964)","journal-title":"Commun. ACM"},{"key":"37_CR28","doi-asserted-by":"crossref","unstructured":"Forsythe, G.E.: Algorithms. Commun. ACM 7(6), 347\u2013349 (1964)","DOI":"10.1145\/512274.512284"},{"key":"37_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-39724-3_19","volume-title":"Correct Hardware Design and Verification Methods","author":"M Gordon","year":"2003","unstructured":"Gordon, M., Hurd, J., Slind, K.: Executing the formal semantics of the accellera property specification language by mechanised theorem proving. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 200\u2013215. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_19"},{"key":"37_CR30","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). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_4"},{"key":"37_CR31","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)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"37_CR32","unstructured":"Haslbeck, M.P.L., Lammich, P.: Refinement with time - refining the run-time of algorithms in Isabelle\/HOL. In: ITP (2019)"},{"key":"37_CR33","unstructured":"Heineman, G., Pollice, G., Selkow, S.: Algorithms in a Nutshell. O\u2019Reilly (2008)"},{"key":"37_CR34","doi-asserted-by":"crossref","unstructured":"Hobor, A., Villard, J.: Ramifications of sharing in data structures. In: POPL (2013)","DOI":"10.1145\/2429069.2429131"},{"key":"37_CR35","unstructured":"Jarn\u00edk, V.: O jist\u00e9m probl\u00e9mu minim\u00e1ln\u00edm. (z dopisu panu o. Bor\u016fvkovi) (1930)"},{"key":"37_CR36","doi-asserted-by":"crossref","unstructured":"Kepner, Jeremy; Gilbert, J.: Graph algorithms in the language of linear algebra. Soc. Ind. Appl. Math. (2011)","DOI":"10.1137\/1.9780898719918"},{"key":"37_CR37","unstructured":"Klasen, V.: Verifying Dijkstra\u2019s algorithm with KeY. Diploma thesis (2010)"},{"key":"37_CR38","unstructured":"Kleinberg, J.M., Tardos, \u00c9.: Algorithm Design. Addison-Wesley (2006)"},{"key":"37_CR39","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL (2017)","DOI":"10.1145\/3009837.3009855"},{"key":"37_CR40","doi-asserted-by":"crossref","unstructured":"Krishna, S., Shasha, D., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. In: POPL (2017)","DOI":"10.1145\/3158125"},{"key":"37_CR41","doi-asserted-by":"crossref","unstructured":"Krishna, S., Summers, A.J., Wies, T.: Local reasoning for global graph properties. In: ESOP (2020)","DOI":"10.26226\/morressier.6052140bb625b5ccab534260"},{"key":"37_CR42","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1090\/S0002-9939-1956-0078686-7","volume":"7","author":"JB Kruskal","year":"1956","unstructured":"Kruskal, J.B.: On the shortest spanning subtree of a graph and the traveling salesman problem. Proc. Am. Math. Soc. 7, 48\u201350 (1956)","journal-title":"Proc. Am. Math. Soc."},{"key":"37_CR43","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). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_21"},{"key":"37_CR44","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). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18"},{"key":"37_CR45","unstructured":"Lammich, P., Nipkow, T.: Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. In: ITP (2019)"},{"key":"37_CR46","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). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_14"},{"issue":"2","key":"37_CR47","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. Reason. 62(2), 261\u2013280 (2019)","journal-title":"J. Autom. Reason."},{"key":"37_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"37_CR49","unstructured":"Leino, K.R.M., Moskal, M.: VACID-0: verification of ample correctness of invariants of data-structures. Edition 0 (2010)"},{"key":"37_CR50","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"37_CR51","doi-asserted-by":"crossref","unstructured":"Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: ICST (2012)","DOI":"10.1109\/ICST.2012.90"},{"key":"37_CR52","unstructured":"Mange, R., Kuhn, J.: Verifying Dijkstra\u2019s algorithm in Jahob (2007)"},{"key":"37_CR53","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). https:\/\/doi.org\/10.1007\/11541868_24"},{"key":"37_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"37_CR55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98047-8_13","volume-title":"Principled Software Development","author":"P M\u00fcller","year":"2018","unstructured":"M\u00fcller, P.: The binomial heap verification challenge in Viper. In: M\u00fcller, P., Schaefer, I. (eds.) Principled Software Development. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_13"},{"key":"37_CR56","unstructured":"M\u00fcller, P.: Private correspondence (2021)"},{"key":"37_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"37_CR58","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s11786-014-0183-z","volume":"9","author":"L Noschinski","year":"2015","unstructured":"Noschinski, L.: A graph library for Isabelle. Math. Comput. Sci. 9, 23\u201339 (2015)","journal-title":"Math. Comput. Sci."},{"key":"37_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"37_CR60","doi-asserted-by":"crossref","unstructured":"Petrank, E., Hawblitzel, C.: Automated verification of practical garbage collectors. Log. Methods Comput. Sci. 6 (2010)","DOI":"10.2168\/LMCS-6(3:6)2010"},{"issue":"6","key":"37_CR61","doi-asserted-by":"publisher","first-page":"1389","DOI":"10.1002\/j.1538-7305.1957.tb01515.x","volume":"36","author":"RC Prim","year":"1957","unstructured":"Prim, R.C.: Shortest connection networks and some generalizations. Bell Syst. Tech. J. 36(6), 1389\u20131401 (1957)","journal-title":"Bell Syst. Tech. J."},{"key":"37_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-319-47958-3_17","volume-title":"Programming Languages and Systems","author":"A Raad","year":"2016","unstructured":"Raad, A., Hobor, A., Villard, J., Gardner, P.: Verifying concurrent graph algorithms. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 314\u2013334. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_17"},{"key":"37_CR63","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"37_CR64","doi-asserted-by":"crossref","unstructured":"Ringer, T., Palmskog, K., Sergey, I., Gligoric, M., Tatlock, Z.: QED at large: a survey of engineering of formally verified software. CoRR (2020)","DOI":"10.1561\/9781680835953"},{"key":"37_CR65","unstructured":"Rosen, K.H.: Discrete Mathematics and Its Applications. 7th edn. (2012)"},{"key":"37_CR66","unstructured":"Sedgewick, R.: Algorithms in C, Part 5: Graph Algorithms (2002)"},{"key":"37_CR67","unstructured":"Sedgewick, R., Wayne, K.: Algorithms. 4th edn. Addison-Wesley (2011)"},{"key":"37_CR68","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-070-4","volume-title":"The Algorithm Design Manual","author":"S Skiena","year":"2008","unstructured":"Skiena, S.: The Algorithm Design Manual, 2nd edn. Springer, Heidelberg (2008)","edition":"2"},{"key":"37_CR69","unstructured":"Tafat, A., March\u00e9, C.: Binary heaps formally verified in Why3 (2011)"},{"issue":"3","key":"37_CR70","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"RE Tarjan","year":"1981","unstructured":"Tarjan, R.E.: A unified approach to path problems. J. ACM 28(3), 577\u2013593 (1981)","journal-title":"J. ACM"},{"key":"37_CR71","unstructured":"Coq development team: The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"37_CR72","unstructured":"Wang, S.: Mechanized verification of graph-manipulating programs. Ph.D. thesis, National University of Singapore (2019)"},{"key":"37_CR73","doi-asserted-by":"crossref","unstructured":"Wang, S., Cao, Q., Mohan, A., Hobor, A.: Certifying graph-manipulating C programs via localizations within data structures. In: OOPSLA (2019)","DOI":"10.1145\/3360597"},{"key":"37_CR74","unstructured":"Wong, W.: A simple graph theory and its application in railway signaling. In: HOL Theorem Proving System and Its Applications (1991)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:29:06Z","timestamp":1626452946000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"290","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":"63","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":"22% - 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":"12","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)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}