Program Verification

• Praxis Critical Systems

• SPARK Examiner

• SPARK Language

  • Ada subset and Annotations

• Proof of program correctness

  • With respect to program pre- and post-conditions

Previous slide

Next slide

Back to first slide

View graphic version