FMitF: Track III: Teaching Program Specifications to the Scientific Computing Community

This project develops educational resources to train the scientific computing community on how to formally describe the expected behavior of scientific programs. The skill of formally specifying program behavior lies at the core of ensuring the correctness of scientific software. Thus, the project impacts improvements in the reliability and quality of scientific software applications. The project’s novelties are in identifying specifications that are relevant to scientific domain experts and implementing a tool that automatically generates tests from those specifications. The investigators apply these discoveries to design and teach an interdisciplinary Vertically Integrated Project course for Boise State University scientific computing students. In addition, the investigators disseminate the produced educational material to the scientific community through workshops and tutorials. The correctness of a scientific program is described by different types of program specifications. This project focuses on identifying and developing the application-level specifications that directly describe computations of physical phenomena. The course material incorporates numerical algorithms written in C and the American National Standards Institute (ANSI) / International Organization for Standardization (ISO) C specification language (ACSL) to express application-level program specifications for those algorithms. A key deliverable of the project is a Frama-C plug-in that generates test cases directly from ACSL specifications. Furthermore, the project explores the sufficiency of ACSL for expressing these application-level specifications. The insights gained from this research will inform the future development of formal methods and tools specifically tailored for scientific software. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.