Professor Cesare Tinelli is co-Principal Investigator for a grant recently awarded by NASA to Rockwell Collins, Inc. and the University of Iowa. Lucas Wagner of Rockwell Collins is the main PI.

The project, entitled "Aspects of Formal Methods Tool Qualification," will investigate issues regarding the assurance and qualification of formal method tools used to aid the development of safety-critical software systems used in avionics. The study will be geared towards the avionic systems guidance document by the Federal Aviation Administration (FAA) titled “Software Considerations in Airborne Systems and Equipment Certification,” published in 2012, and its related supplements. Professor Tinelli's team will focus on producing artifacts for a specific open source formal verification tool, the Kind 2 model checker, and investigating with the Rockwell Collins collaborators the feasibility of qualifying its outputs through the generation of formal proof certificates that can be checker by third party, trusted proof checker.

The Iowa portion of two-year project has been awarded $269,176.