{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:24:30Z","timestamp":1764350670271,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030888053"},{"type":"electronic","value":"9783030888060"}],"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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88806-0_17","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"346-358","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Automated Verification of the Parallel Bellman\u2013Ford Algorithm"],"prefix":"10.1007","author":[{"given":"Mohsen","family":"Safari","sequence":"first","affiliation":[]},{"given":"Wytse","family":"Oortwijn","sequence":"additional","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,13]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Agarwal, P., Dutta, M.: New approach of Bellman Ford algorithm on GPU using compute unified design architecture (CUDA). Int. J. Comput. Appl. 110(13) (2015)","DOI":"10.5120\/19375-1027"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and verification of atomic operations in GPGPU programs. In: SEFM, vol. 9276 (2015)","DOI":"10.1007\/978-3-319-22969-0_5"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87\u201390 (1958)","DOI":"10.1090\/qam\/102435"},{"issue":"2","key":"17_CR4","first-page":"1","volume":"12","author":"MA Bender","year":"2015","unstructured":"Bender, M.A., Fineman, J.T., Gilbert, S., Tarjan, R.E.: A new approach to incremental cycle detection and related problems. ACM Trans. Algorith. (TALG) 12(2), 1\u201322 (2015)","journal-title":"ACM Trans. Algorith. (TALG)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA, pp. 113\u2013132. ACM (2012)","DOI":"10.1145\/2398857.2384625"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs. Sci. Comput. Prog. 95, 376\u2013388 (2014)","journal-title":"Sci. Comput. Prog."},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"issue":"8","key":"17_CR9","doi-asserted-by":"publisher","first-page":"2222","DOI":"10.1109\/TPDS.2015.2485994","volume":"27","author":"F Busato","year":"2016","unstructured":"Busato, F., Bombieri, N.: An efficient implementation of the Bellman-Ford algorithm for Kepler GPU architectures. IEEE Trans. Parall. Distrib. Syst. 27(8), 2222\u20132233 (2016)","journal-title":"IEEE Trans. Parall. Distrib. Syst."},{"key":"17_CR10","unstructured":"Chen, R., Cohen, C., L\u00e9vy, J.J., Merz, S., Th\u00e9ry, L.: Formal proofs of Tarjan\u2019s algorithm in Why3, Coq, and Isabelle. arXiv preprint arXiv:1810.11979 (2018)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-34188-5_18","volume-title":"Hardware and Software: Verification and Testing","author":"P Collingbourne","year":"2012","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic testing of openCL code. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 203\u2013218. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_18"},{"key":"17_CR12","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/"},{"key":"17_CR13","unstructured":"Dafny program verifier, https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/"},{"issue":"1","key":"17_CR14","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. Numerische mathematik 1(1), 269\u2013271 (1959)","journal-title":"Numerische mathematik"},{"key":"17_CR15","unstructured":"Ford, L.R., Jr.: Network flow theory. Tech. rep, DTIC Document (1956)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-662-49674-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Grov","year":"2016","unstructured":"Grov, G., Tumas, V.: Tactics for the Dafny program verifier. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 36\u201353. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_3"},{"key":"17_CR17","unstructured":"Gu\u00e9neau, A., Jourdan, J.H., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Interactive Theorem Proving. No. 141, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Hajela, G., Pandey, M.: Parallel implementations for solving shortest path problem using Bellman-Ford. Int. J. Comput. Appl. 95(15) (2014)","DOI":"10.5120\/16667-6659"},{"key":"17_CR19","unstructured":"Isabelle interactive theorem prover. http:\/\/isabelle.in.tum.de\/index.html"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Jeong, I.K., Uddin, J., Kang, M., Kim, C.H., Kim, J.M.: Accelerating a Bellman-Ford routing algorithm using GPU. In: Frontier and Innovation in Future Computing and Communications, pp. 153\u2013160. Springer (2014)","DOI":"10.1007\/978-94-017-8798-7_19"},{"key":"17_CR21","unstructured":"Kleinberg, J., Tardos, E.: Algorithm design. Pearson Education India, New Delh (2006)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-24372-1_23","volume-title":"Automated Technology for Verification and Analysis","author":"A Laarman","year":"2011","unstructured":"Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 321\u2013335. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_23"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Lammich, P., Neumann, R.: A Framework for Verifying Depth-First Search Algorithms. In: CPP, pp. 137\u2013146. ACM (2015)","DOI":"10.1145\/2676724.2693165"},{"key":"17_CR24","unstructured":"Lammich, P., Wimmer, S.: IMP2-simple program verification in Isabelle\/HOL. Archive of Formal Proofs (2019)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: SIGSOFT FSE 2010, Santa Fe, pp. 187\u2013196. ACM (2010)","DOI":"10.1145\/1882291.1882320"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: ACM SIGPLAN Notices. vol. 47, pp. 215\u2013224. ACM (2012)","DOI":"10.1145\/2370036.2145844"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Oortwijn, W.: Deductive techniques for model-based concurrency verification. Ph.D. thesis, University of Twente, Netherlands (2019). https:\/\/doi.org\/10.3990\/1.9789036548984","DOI":"10.3990\/1.9789036548984"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-030-45190-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Huisman, M., Joosten, S.J.C., van de Pol, J.: Automated verification of parallel nested DFS. In: TACAS 2020. LNCS, vol. 12078, pp. 247\u2013265. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_14"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"van de Pol, J.C.: Automated verification of nested DFS. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 181\u2013197. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19458-5_12","DOI":"10.1007\/978-3-319-19458-5_12"},{"key":"17_CR30","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":"17_CR31","doi-asserted-by":"crossref","unstructured":"Safari, M., Oortwijn, W., Huisman, M.: Artifact for automated verification of the parallel bellman-ford algorithm. In: SAS (2021). https:\/\/github.com\/Safari1991\/SSSP-Verification","DOI":"10.26226\/morressier.604907f51a80aac83ca25d80"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-68953-1_5","volume-title":"Topics in Theoretical Computer Science","author":"M Safari","year":"2017","unstructured":"Safari, M., Ebnenasir, A.: Locality-based relaxation: an efficient method for GPU-based computation of shortest paths. In: Mousavi, M.R., Sgall, J. (eds.) TTCS 2017. LNCS, vol. 10608, pp. 43\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68953-1_5"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77\u201387 (2015)","DOI":"10.1145\/2813885.2737964"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Surve, G.G., Shah, M.A.: Parallel implementation of bellman-ford algorithm using CUDA architecture. In: 2017 International conference of Electronics, Communication and Aerospace Technology (ICECA), vol. 2, pp. 16\u201322. IEEE (2017)","DOI":"10.1109\/ICECA.2017.8212794"},{"key":"17_CR35","doi-asserted-by":"crossref","unstructured":"Volkov, G., Mandrykin, M., Efremov, D.: Lemma functions for Frama-c: C programs as proofs. In: 2018 Ivannikov Ispras Open Conference (ISPRAS), pp. 31\u201338. IEEE (2018)","DOI":"10.1109\/ISPRAS.2018.00012"},{"key":"17_CR36","unstructured":"A Theory of Bellman-Ford, in Isabelle. https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Monad_Memo_DP\/Bellman_Ford.html. Accessed Jan 2021"},{"key":"17_CR37","unstructured":"Why3 gallery of formally verified programs. http:\/\/toccata.lri.fr\/gallery\/graph.en.html"},{"key":"17_CR38","unstructured":"Why3 program verifier. http:\/\/why3.lri.fr\/"},{"key":"17_CR39","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). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_34"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88806-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:39:25Z","timestamp":1634146765000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88806-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888053","9783030888060"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88806-0_17","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":"13 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/staticanalysis.org\/","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":"40","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":"18","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":"4","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":"45% - 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)"}}]}}