Verifying Fortran Programs with CIVL
- Open Access
- 2022
- OriginalPaper
- Buchkapitel
- Verfasst von
- Wenhao Wu
- Jan Hückelheim
- Paul D. Hovland
- Stephen F. Siegel
- Verlag
- Springer International Publishing
Zusammenfassung
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’s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application.
- Titel
- Verifying Fortran Programs with CIVL
- Verfasst von
-
Wenhao Wu
Jan Hückelheim
Paul D. Hovland
Stephen F. Siegel
- Copyright-Jahr
- 2022
- Buch
-
Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-030-99523-2
Electronic ISBN: 978-3-030-99524-9
Copyright-Jahr: 2022
- DOI
- https://doi.org/10.1007/978-3-030-99524-9_6
