For the final exam the students should:

- be able to use verification by proof method to prove partial or total correctness

- know the terminology of verification by proof and inference rules

- know the kinds of symbolic evaluation method (path-dependent and global); know their advantages and weaknesses

- be able to use a path dependent symbolic evaluation method

- know the principle of operation of a satisfiability based verification method implemented in Alloy (diagram from the corresponding set of slides)

- describe the operation of the FLAVERS approach using a simple example (e.g. the one from the slides)

- describe relative advantages and disadvantages of FLAVERS data flow finite state verification and model checking

- know what is meant by precision in the FLAVERS approach

- know why a Control Flow Graph is considered to overapproximate programs behavior and what kind of a problem that creates for interpretation of FLAVERs analysis results

- know what purpose a contstraint FSA serves (something dealing with infeasible paths)

- know the computational complexity of a model checking algorithm (linear in the size of the model and in the size of the formula, but the model size grows exponentially e.g. in the number of if-statements) and FLAVERS approach with constraint FSAs (O(N^2 × Sp× Sc1 ×…× Scn), where N - number of nodes in an CFG, Sp - number of nodes ina property FSA, Sci - number of nodes in an "ith" constraint FSA)

- know the relative advantages and weaknesses of methods discussed in class