{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:44:58Z","timestamp":1743011098767,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran\u2019s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_6","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"106-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Fortran Programs with CIVL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9087-4240","authenticated-orcid":false,"given":"Wenhao","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3479-6361","authenticated-orcid":false,"given":"Jan","family":"H\u00fcckelheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0907-2567","authenticated-orcid":false,"given":"Paul D.","family":"Hovland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9359-3332","authenticated-orcid":false,"given":"Stephen F.","family":"Siegel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Adams, J.C., Brainerd, W.S., Hendrickson, R.A., Maine, R.E., Martin, J.T., Smith, B.T.: The Fortran 2003 Handbook: the Complete Syntax, Features and Procedures. Springer Science & Business Media (2008). https:\/\/doi.org\/10.1007\/978-1-84628-746-6","DOI":"10.1007\/978-1-84628-746-6"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Baranov\u00e1, Z., Barnat, J., Kejstov\u00e1, K., Ku\u010dera, T., Lauko, H., Mr\u00e1zek, J., Ro\u010dkai, P., \u0160till, V.: Model checking of C and C++ with DIVINE 4. In: Automated Technology for Verification and Analysis. LNCS, vol. 10482, pp. 201\u2013207. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14","DOI":"10.1007\/978-3-319-68167-2_14"},{"key":"6_CR3","doi-asserted-by":"publisher","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\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium (FMCO 2005). Lecture Notes in Computer Science, vol.\u00a04111, pp. 364\u2013387. Springer (2005). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, pp. 171\u2013177. Springer (2011), http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032319","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"6_CR5","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages. pp. 53\u201364. Wroc\u0142aw, Poland (August 2011), http:\/\/proval.lri.fr\/publications\/boogie11final.pdf."},{"key":"6_CR6","unstructured":"Boyer, R.S., Moore, J.S.: A verification condition generator for Fortran. Tech. Rep. CSL-103, SRI International, Computer Science Laboratory, Menlo Park, CA (June 1980), https:\/\/apps.dtic.mil\/sti\/pdfs\/ADA094609.pdf"},{"key":"6_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. Proc. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908) (2008)"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 215\u2013222 (May 1976). https:\/\/doi.org\/10.1109\/TSE.1976.233817","DOI":"10.1109\/TSE.1976.233817"},{"key":"6_CR9","unstructured":"Cleanscape Software International: FORTRAN-lint: a pre-compile analysis tool, https:\/\/stellar.cleanscape.net\/docs_lib\/data_F-lint2.pdf, accessed 13-Oct-2021"},{"key":"6_CR10","unstructured":"Dingle, N.: Not only Fortran and MPI: POP\u2019s view of HPC software in Europe, https:\/\/pop-coe.eu\/blog\/not-only-fortran-and-mpi-pops-view-of-hpc-software-in-europe, accessed 14-Oct-2021"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Feldman, S.I.: A Fortran to C converter. SIGPLAN Fortran Forum 9(2), 21\u201322 (Oct 1990). https:\/\/doi.org\/10.1145\/101363.101366","DOI":"10.1145\/101363.101366"},{"key":"6_CR12","unstructured":"Flang Fortran language front-end. https:\/\/github.com\/flang-compiler\/flang, accessed 09-Oct-2021"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Garzella, J.J., Baranowski, M., He, S., Rakamari\u0107, Z.: Leveraging compiler intermediate representation for multi- and cross-language verification. In: Beyer, D., Zufferey, D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 90\u2013111. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_5","DOI":"10.1007\/978-3-030-39322-9_5"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Grosse-Kunstleve, R.W., Terwilliger, T.C., Sauter, N.K., Adams, P.D.: Automatic Fortran to C++ conversion with FABLE. Source Code for Biology and Medicine 7(5) (2012). https:\/\/doi.org\/10.1186\/1751-0473-7-5","DOI":"10.1186\/1751-0473-7-5"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: A framework for verifying C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a09035, pp. 447\u2013450. Springer Berlin Heidelberg, Berlin, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_41","DOI":"10.1007\/978-3-662-46681-0_41"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization (CGO\u201904). pp. 75\u201386. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"6_CR17","unstructured":"Lawrence Livermore National Laboratory: CORAL benchmark codes (2014), https:\/\/asc.llnl.gov\/coral-benchmarks, accessed 14-Oct-2021"},{"key":"6_CR18","unstructured":"Message Passing Interface Forum: MPI: A Message-Passing Interface standard, version 3.1 (Jun 2015), https:\/\/www.mpi-forum.org\/docs\/mpi-3.1\/mpi31-report.pdf"},{"key":"6_CR19","unstructured":"Moniot, R.K.: ftnchek: a static analyzer for Fortran 77, https:\/\/www.dsm.fordham.edu\/~ftnchek\/, accessed 09-Oct-2021"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR21","unstructured":"NEK5000: a fast and scalable high-order solver for computational fluid dynamics (2021), https:\/\/nek5000.mcs.anl.gov, accessed 14-Oct-2021"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Nguyen, T.V.N., Irigoin, F.: Alias verification for Fortran code optimization. Electronic Notes in Theoretical Computer Science 65(2), 52\u201366 (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80396-7, COCV\u201902, Compiler Optimization Meets Compiler Verification (Satellite Event of ETAPS 2002)","DOI":"10.1016\/S1571-0661(04)80396-7"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Noller, Y., P\u0103s\u0103reanu, C.S., Fromherz, A., Le, X.B.D., Visser, W.: Symbolic Pathfinder for SV-COMP. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 239\u2013243. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_21","DOI":"10.1007\/978-3-030-17502-3_21"},{"key":"6_CR24","unstructured":"NVIDIA: CUDA Toolkit Documentation, v11.4.2, https:\/\/docs.nvidia.com\/cuda\/, accessed 14-Oct-2021"},{"key":"6_CR25","unstructured":"Open Group: IEEE Std 1003.1: Standard for information technology\u2014Portable Operating System Interface (POSIX(R)) base specifications, issue 7: pthread.h (2018), https:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/basedefs\/pthread.h.html"},{"key":"6_CR26","unstructured":"OpenMP Architecture Review Board: OpenMP Application Programming Interface (Nov 2020), https:\/\/www.openmp.org\/wp-content\/uploads\/OpenMP-API-Specification-5-1.pdf, version 5.1"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Orchard, D., Contrastin, M., Danish, M., Rice, A.: Verifying spatial properties of array computations. Proceedings of the ACM on Programming Languages 1(OOPSLA), 1\u201330 (Oct 2017). https:\/\/doi.org\/10.1145\/3133899, article no. 75","DOI":"10.1145\/3133899"},{"key":"6_CR28","unstructured":"Parr, T.: The Definitive ANTLR4 Reference. The Pragmatic Bookshelf, Dallas, TX (2013), https:\/\/pragprog.com\/titles\/tpantlr2\/the-definitive-antlr-4-reference\/"},{"key":"6_CR29","unstructured":"Polyhedron Solutions: Linux Fortran compiler diagnostic comparisons, https:\/\/www.fortran.uk\/fortran-compiler-comparisons\/intellinux-fortran-compiler-diagnostic-capabilities\/, accessed 13-Oct-2021"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: Decoupling source language details from verifier implementation. In: Biere, A., Bloem, R. (eds.) Proceedings of the 26th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a08559, pp. 106\u2013113. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"6_CR31","unstructured":"Rasmussen, C.E., et\u00a0al.: OFP: Open Fortran Project, https:\/\/sourceforge.net\/p\/fortran-parser\/wiki\/Home\/, accessed 14-Oct-2021"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Rosner, R., Calder, A., Dursi, L., Fryxell, B., Lamb, D., Niemeyer, J., Olson, K., Ricker, P., Timmes, F., Truran, J., Tufo, H., Young, Y.N., Zingale, M., Lusk, E., Stevens, R.: Flash code: Studying astrophysical thermonuclear flashes. Computing in Science and Engineering 2, 33\u201341 (2000). https:\/\/doi.org\/10.1109\/5992.825747","DOI":"10.1109\/5992.825747"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Siegel, S.F., Zheng, M., Luo, Z., Zirkel, T.K., Marianiello, A.V., Edenhofner, J.G., Dwyer, M.B., Rogers, M.S.: CIVL: The Concurrency Intermediate Verification Language. In: SC15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. ACM, New York (Nov 2015). https:\/\/doi.org\/10.1145\/2807591.2807635, article no. 61, pages 1\u201312","DOI":"10.1145\/2807591.2807635"},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"Sinz, C., Merz, F., Falke, S.: LLBMC: A bounded model checker for LLVM\u2019s intermediate representation. In: Flanagan, C., K\u00f6nig, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a07214, pp. 542\u2013544. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_44","DOI":"10.1007\/978-3-642-28756-5_44"},{"key":"6_CR35","unstructured":"Synopsys: Synopsys static analysis (Coverity) Fortran syntax analysis, https:\/\/community.synopsys.com\/s\/article\/Synopsys-Static-Analysis-Coverity-Fortran-Syntax-Analysis, accessed 13-Oct-2021"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Verma, G., Shi, Y., Liao, C., Chapman, B., Yan, Y.: Enhancing DataRaceBench for evaluating data race detection tools. In: 2020 IEEE\/ACM 4th International Workshop on Software Correctness for HPC Applications (Correctness). pp. 20\u201330. IEEE (2020). https:\/\/doi.org\/10.1109\/Correctness51934.2020.00008","DOI":"10.1109\/Correctness51934.2020.00008"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:18:19Z","timestamp":1648534699000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","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":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","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":"159","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":"46","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":"29% - 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":"10","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 of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","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)"}}]}}