FMitF: Track II: Usability, Robustness, and Performance Improvements for CIVL

University Of Delaware, Newark DE

Investigators

Abstract

Scientific and high-performance computing software deals with issues of fundamental importance to science, engineering, and society more generally. Examples include applications to predict earthquake damage, model the global climate, perform atomic-level simulations of chemical and biological systems, and to investigate the electronic structure of matter. These programs inform both profound scientific conclusions and decisions of the utmost importance to society. For these reasons, it is imperative to develop effective methods for debugging and verifying scientific programs. This project enhances the usability, performance, and robustness of the Concurrent Intermediate Verification Language (CIVL), a verification tool for scientific programs based on symbolic execution and model checking. The project's novelties are (1) an expanded ability to verify programs that use a variety of parallel-programming Application Programming Interfaces (APIs), and (2) the capability to verify that two versions of a program are equivalent. The project's impacts are seen in the improved productivity of the software developers using CIVL to help debug their code, and in the increased confidence in the correctness of the resulting software. The project improves CIVL along three lines: usability, robustness and language coverage, and performance. Usability improvements include improved error reporting and the ability to control precisely what CIVL checks. Language coverage is improved by correcting limitations in CIVL's array model, and increasing coverage of the C standard library. Performance is being improved by parallelizing CIVL's model-checking engine and streamlining its expression-evaluation algorithm. These improvements are guided by ongoing interaction with scientific-software development teams who are using CIVL and providing feedback. 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.