F-IKOS: An Abstract Interpretation-based Static Analyzer for Fortran Programs
by Sheng Zou, Liqian Chen, Guangsheng Fan, Renjie Huang, and Banghu Yin
presented at the workshop Quantitative Approaches to Software Quality 2024
Abstract: The Fortran programming language is widely utilized in numerical computation and scientific computing. Fortran programs are prone to potential runtime errors related to numerical properties due to the large number of numerical operations. In this paper, we present F-IKOS, an abstract interpretation-based static analyzer for Fortran programs on top of IKOS, which soundly handles floating-point types in Fortran programs. Firstly, we translate Fortran programs to LLVM IR using compiler front-end Flang. After that, we extend IKOS to support sound floating-point analysis and then employ it to analyze the translated LLVM IR. Particularly, when analyzing f loating-point types in programs, we first abstract floating-point expressions into real-number expressions with interval coefficients, and then linearize these expressions into real-number expressions with scalar coefficients. These linear expressions are subsequently handled by abstract domains originally designed for real-number types to produce sound analysis results. We have conducted experiments on representative Fortran programs to show the efficiency and effectiveness of F-IKOS. The experimental results are encouraging: F-IKOS soundly analyzes runtime errors in complex programs, outperforming other analyzers.
Keywords Fortran, Static Analysis, Abstract Interpretation, Floating-point Program Analysis
I don’t know how to obtain F-IKOS, but it is an offshoot of
They tested their tool on the FortranTip codes 
(among other codes).