Introduction
	• Correctness by Construction – Bugs are cheaper if discovered early – Push more cost to the front • Example: Lockheed C130J Software – 1/10 of average bugs found in FAA testing – Productivity improvement of factor of four – ½ Development of non-safety critical development costs