Formalising Design/Verification

This session introduces the use of proof in B and shows how specifications and designs can be verified for internal consistency and refinement. The use of model-checking to verify temporal properties is also introduced.