Certifiable Program Sythesis at NASA

Certification Approach

• Generate code and the detailed annotations
• Generate safety obligations from annotated code
• Safety obligations are provable iff the code is safe

Application of ATP

• Safety obligations generated in TPTP format
• SSCPA used to find proofs
• GDV used to verify proofs
• Proofs form (part of) certification for authorities, e.g., FAA
• Problems added to the TPTP problem library