the tool checks each code instruction by taking into account all possible values of every variable at every point in the code,providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions.