Proving Process
	• Verification Conditions (VCs) generated – Some via run-time check (RTC) generator: array index out of range, type range violation, division by zero, and numerical overflow. – Others to ensure post-conditions hold • Simplifier dispatches as many as possible • Proof Checker for rest