Formal Methods in Software Development

The course can be part of the following programmes:

1. Computer Science, Master's Programme (N2COS)
2. Computer Science, Bachelor's Programme (N1COS)

The course is a also a single-subject course at Gothenburg University.

Successfully completed courses corresponding to 120 credits within the subject Computer Science or equivalent, specifically DIT201 Logic in Computer Science, 7.5 credits, and a 7.5 credits course in object-oriented programming (or equivalent) are required.

Applicants must prove knowledge of English: English 6/English level 2 or the equivalent level of an internationally recognized test, for example TOEFL, IELTS.

The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.

On the model checking side, we cover the following topics:

• a specification language for concurrent processes,
• verifying assertions,
• synchronization,
• verifying safety and liveness properties in temporal logic.

On the deductive verification side, we cover the following topics:

• program logics, including Hoare logic and separation logic,
• reasoning about loops using invariants,
• verification of small programs using tools for program verification
• techniques used when tackling verification of larger or more complex programs

On successful completion of the course the student will be able to:

Knowledge and understanding

• explain the potential and limitations of using logic based verification methods for assessing and improving software correctness,
• identify what can and what cannot be expressed by certain specification/modeling formalisms,
• identify what can and cannot be analyzed with certain logics and proof methods,

Competence and skills

• express safety and liveness properties of (concurrent) programs in a formal way,
• describe the basics of verifying safety and liveness properties via model checking,
• successfully employ tools which prove or disprove temporal properties,
• write formal specifications of object-oriented system units, using the concepts of method contracts and class invariants,
• describe how the connection between programs and formal specifications can be represented in a program logic,
• verify functional properties of simple programs in a verification tool

Judgement and approach

• judge and communicate the significance of correctness for software development,
• employ abstraction, modelling, and rigorous reasoning when approaching the development of correctly functioning software.

There are about two lectures each week, and one exercise class per week. The students perform practical case studies using the tools in the laboratory assignments.

Language of instruction: English

The course is examined by a written hall exam and compulsory laboratory assignments handed in during the course. The practical laboratory assignments are normally carried out in pairs.

If a student who has been failed twice for the same examination element wishes to change examiner before the next examination session, such a request is to be granted unless there are specific reasons to the contrary (Chapter 6 Section 22 HF).

If a student has received a certificate of disability study support from the University of Gothenburg with a recommendation of adapted examination and/or adapted forms of assessment, an examiner may decide, if this is consistent with the course’s intended learning outcomes and provided that no unreasonable resources would be needed, to grant the student adapted examination and/or adapted forms of assessment.

If a course has been discontinued or undergone major changes, the student must be offered at least two examination sessions in addition to ordinary examination sessions. These sessions are to be spread over a period of at least one year but no more than two years after the course has been discontinued/changed. The same applies to placement and internship (VFU) except that this is restricted to only one further examination session.

If a student has been notified that they fulfil the requirements for being a student at Riksidrottsuniversitetet (RIU student), to combine elite sports activities with studies, the examiner is entitled to decide on adaptation of examinations if this is done in accordance with the Local rules regarding RIU students at the University of Gothenburg.

Sub-courses

1. Written hall exam, 5 credits
   Grading scale: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U)
2. Laboratory, 2.5 credits
   Grading scale: Pass (G) and Fail (U)

The grading scale comprises: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U).

To pass the whole course, it is necessary to pass both the written hall examination and the labs. In case of pass, the grade is determined by the result in the written hall examination.

The course is evaluated through meetings both during and after the course between teachers and student representatives. Further, an anonymous questionnaire is used to ensure written information. The outcome of the evaluations serves to improve the course by indication which parts could be added, improved, changed or removed.

The course is a joint course together with Chalmers.

The course replaces the DIT271 Software Engineering using Formal Methods course. The course cannot be included in a degree which contains DIT271. Neither can the course be included in a masterdegree which is based on a bachelordegree in which the course DIT271 is included.