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

- Apply common software testing techniques such as equivalence classes, boundary-value analysis, coverage metrics

- Use assertions in software development to increase software quality

- Specify and prove software correct using pre- and post-conditions, invariants, and Hoare Logic

- Apply automated software verification techniques such as Bounded Model Checking and Symbolic Simulation

• Methods for modeling and specificatoin by logic, automaton, assertions and coverage criteria.
• verification tools, (model checker, static analysis, theorem proof, testing)
• Practical experiences with verification tools
• Basics about certification and  standards concerning industrial validitation

- Solving of exercises

- Use of software verification tools to automatically detect software bugs

The lecture will be held in-person. LectureTube recordings will be made available on TUWEL.

ECTS Breakdown:

36h Lectures
114h Exercises
---------------------------
150h total (6 ECTS)
---------------------------

The students will solve and hand in exercise sheets (includiing pencil-and-paper exercises as well as practical tasks such as applying software verification tools). The solutions are marked and annotated with feedback.