The analysis and verification of software systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality. Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software.

 

The goal of this course is to provide an introduction to the field of formal semantics for programming languages, with particular emphasis on software verification. The following topics will be covered:

Basic knowledge in the following areas is expected:

The exercise sheets will be made available on Mondays. Please hand in your solution in before the beginning of the exercise classes, i.e., on Monday before 10:00 am.

Admission to the examination requires at least 50 % of the points in the exercises.

  Hand in April 22

  Hand in May 13

  Hand in May 27

  Hand in June 10 (since there will be no exercise class on June 10, please hand in your answer sheets in Room 4207)

  Hand in June 24

  Hand in July 1

  Hand in July 8. Transition relation graph for exercise 3(b):

  Hand in July 15

 

 

 

Any students not mentioned, were below 50%.

The exam is organized in oral form. The following periods arre offered:

• Mon 22 July - Fri 26 July
• Thu 15 August - Wed 21 August
• Wed 4 September - Fri 11 October

Please contact Thomas Noll directly for arranging an appointment. Registration is possible via Campus.