Wenhao Wu, Jan Hückelheim, Paul D. Hovland, and Stephen
F. Siegel. Tools and Algorithms for the Construction and
Analysis of Systems: 28th International Conference, TACAS 2022, Held
as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings,
Part I. Lecture Notes in Computer Science 13243,
pp. 106-124. Springer, Cham, 2022.
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.
@inproceedings{wu-etal:2022:fortran,
author = {Wu, Wenhao and H\"{u}ckelheim, Jan and Hovland, Paul D.
and Siegel, Stephen F.},
title = {Verifying {F}ortran Programs with {CIVL}},
year = {2022},
publisher = {Springer},
address = {Cham},
doi = {10.1007/978-3-030-99524-9_6},
booktitle = {Tools and Algorithms for the Construction and Analysis
of Systems (TACAS 2022)},
series = {Lecture Notes in Computer Science},
volume = 13243,
pages = {106--124},
location = {Munich, Germany}
}
