Motivation How to verify the safety correctness properties of low-level system software? System Java (JML) C#(Spec # Software Cyclone CCured TAL Vanilla CC++&Assembly? HardwareMotivation How to verify the safety & correctness properties of low-level system software? Vanilla C & C++ & Assembly? Hardware Java (JML) C# (Spec #) Cyclone CCured TAL System … Software