After successful completion of the course, students are able to...

• ... formalise Problems as SAT or SMT problems,
• ... to solve the formalistaions with Z3,
• ... solve combinbatorial problems via a reduction und SAT-solving tools,
• ... to apply deductive verification methods based on Hoare logic and predica transformers, 
• ... to establish partial/total correctness of software using deductive verification methods and tools,
• ... to apply model checking: to create a model of the system that needs to be verified, to formalize the specification as a formula in temporal logic, and to interpret possible counterexamples.

This course deepens the understanding of the topics in the course "6.0 VU Formal Methods in Computer Science" by offering additional exercises. The course presents exercises for the following topics:

• Complexity theory: NP-completeness, undecidability, reduction of problems
• Satisfiability problems: SAT, SMT
• Partial/total correctness of programs: Hoare calculus, weakest precondition, strongest postcondition
• Formal verification based on model checking

For each of the topics, there is an exercise sheet.

• Each of the exercises sheets will be presented in a dedicated class.
• Students are supposed to work on these exercises autonomously and submit their solutions in tuwel.
• There will be a class where student solutions and an example solution are discussed.

Kick-off: 3.10.2023, 13:00 (together via VU, EI5)

The submitted solutions to each of the exercise sheets are graded, on a scale of 0-15 points each. The scoring depends on the correctness of the solutions as well as the on the quality of writing of the accompanying report. The final grad is by the sum of the points for the individual exercise sheets.

This course builds on the material taught in the VU Formal Methods in Computer Science. Students of this course are supposed to take the VU Formal Methods in Computer Science in parallel.