Static Analysis for Verification of Safety Properties of Critical Software

Critical software must satisfy certain safety properties. A safety property ensures that something bad never happens during the execution of the software. This study proposes to use semantics-based static analysis to derive conditions for fulfillment of safety properties of critical software based on an innovative approach we have developed for deriving conditions for error-free execution of programs. The impact of this study lies in the development of better techniques for verification and diagnosis of critical software.

Supported by Michigan Space Grant Consortium