NASA Logo, National Aeronautics and Space Administration


The objective of this project is to apply and develop analytic verification technology. Analytic tools rely on algorithms that mathematically analyze specifications, code, and models for consistency with requirements and designs. This provides a complementary and higher level of debugging and V&V than traditional testing methods alone.

The goal of this project is to develop and apply automated tools, such as model checkers and static analyzers, in the verification and validation of critical software systems.

Technologies of interest:

  • Model Checking
  • Theorem Proving
  • Static Analysis
  • Abstract Interpretation
  • Runtime Verification
  • Automated Abstraction
  • Invariant Generation
  • Learning-based testing
For applications in:
  • Formalization of architectures
  • Safety Assurance and safety cases
  • Machine learning assurance
  • Autonomy assurance
  • Model (Simulink) V&V
  • Code V&V
  • Requirement elicitation, formalization and analysis
  • Process improvement: traceability, and dashboard summary.


Group Lead
Guillaume P Brat

First Gov logo
NASA Logo -