There is a flourishing ecosystem of verification tools for C programs, but very little for Fortran, which is widely used in high performance computing. In this work, we have extended the CIVL model checker, a well-known verifier for sequential and concurrent C programs, to Fortran. We have developed a Fortran front-end tailored for verification, as opposed to translation to machine code. This defect-preserving front-end has advantages over compiler-based tools, which may “compile away” program defects.
Significance and Impact
Based on a study involving 35 benchmarks, our new CIVL-based tool is faster and able to detect defects missed by earlier tools. We also applied CIVL to code from a leading computational fluid dynamics application, Nek5000. We used CIVL to verify matrix multiplication routines, and to prove that a numerical quadrature implemented in Nek5000 has the claimed order of accuracy, among other properties.
Verification time (seconds) for CIVL (red striped) vs. SMACK (blue) on a Fortran verification benchmark suite. Lower is better. No bar is shown when a tool could not complete a verification task. Each time is the mean over 5 of 7 executions after dropping the shortest and longest.
Technical Approach
A front-end that translates Fortran source to CIVL-C, the intermediate verification language used by the CIVL model checker
Precise modeling of Fortran array semantics, pass-by-value vs. pass-by-reference, variable attributes, and other language features unique to Fortran
Verifying Fortran Programs with CIVL. Wenhao Wu, Jan Hückelheim, Paul D. Hovland, and Stephen F. Siegel, TACAS 2022. doi: 10.1007/978-3-030-99524-9_6. Badges: EAPLS Artifacts Available and EAPLS Artifacts Evaluated and Reusable, v1.1.