Lockheed C130J
	• Operational Flight Program (OFP) software co- ordinates and controls most of the avionics systems and operates and diagnoses the integrated aircraft. • Little true verification – Used a precise language – Spark – Forced programmers to write flow annotations – Used flow analysis on top of syntactic and static analysis. – Proved Exception free.