Description:

Students are able to describe semantics of software formally and to use sound reasoning for construction of correct software. They learn to use some software tools that allow to prove basic properties of software.

Contents:

1. Introduction to formal program specification
2. Proof methods
3. Logical theories and modeling of data structures
4. Operational program semantics
5. Unbounded software model checking
6. (2) Unbounded software model checking
7. Functions, procedures
8. Termination proofs
9. Symbolic execution
10. Decision procedures
11. Object oriented programming
12. Program synthesis

Seminar contents:

Practical training of the lecture material.

Recommended literature:

1. Clarke, E.M. - Henzinger, Th.A. - Veith, H. - Bloem, R. (Eds.) : Handbook of Model Checking. Springer,
2018. ISBN 978-3-319-10574-1.
2. Kroening, D. - Strichman, O. : Decision Procedures - An Algorithmic Point of View, 2nd edition. Springer,
2016. ISBN 978-3-662-50496-3.
3. Bradley, A. R. - Manna, Z. : The Calculus of Computation. Springer, 2007. ISBN 978-3-540-74113-8.

Abbreviations used:

Semester:

• W ... winter semester (usually October - February)
• S ... spring semester (usually March - June)
• W,S ... both semesters

Mode of completion of the course:

• A ... Assessment (no grade is given to this course but credits are awarded. You will receive only P (Passed) of F (Failed) and number of credits)
• GA ... Graded Assessment (a grade is awarded for this course)
• EX ... Examination (a grade is awarded for this course)
• A, EX ... Examination (the award of Assessment is a precondition for taking the Examination in the given subject, a grade is awarded for this course)

Weekly load (hours per week):

• P ... lecture
• C ... seminar
• L ... laboratory
• R ... proseminar
• S ... seminar