a) Draw the Control Flow Automaton (CFA) model of the program sample. Use the numbers specified next to the statements (0, 1, 2) to label the CFA locations. Use a specific location err for the case when there is division with zero in statement 2, and location end for the normal termination of the program. 0: 1: 2: b int b = 25 while (25 b*b < 0) { } b = (b+25/b)/2; b) For model checking of the CFA we use location and predicate abstraction, using a single predicate (b==0). Decide whether the following path appears in the abstract state space (justify your answer): (0, true) (1, false) (2, true) (err, true). c) Someone claims that in the abstract state space he found the following counterexample to the correct behavior of the program: (0, false) (1, false) (2, false) (err, false). Check whether this path can be traversed in the concrete state space (justify your answer).