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
• Slicing (semantic and syntactic)
• Formalization of architectures