Provably Correct Software

10 credits

Syllabus, Master's level, 1DL430

Code
1DL430
Education cycle
Second cycle
Main field(s) of study and in-depth level
Computer Science A1N
Grading system
Fail (U), Pass (3), Pass with credit (4), Pass with distinction (5)
Finalised by
The Faculty Board of Science and Technology, 30 August 2018
Responsible department
Department of Information Technology

Entry requirements

120 credits including Program design, Algebra, Logic and Proof Techniques, Algorithms and Data Structures, Programming Theory (or equivalent courses). Proficiency in English equivalent to the Swedish upper secondary course English 6.

Learning outcomes

On completion of the course, the student should be able to:

  • understand how formal methods fit into the software development process,
  • explain the principles of model-based specification and refinement-based program development,
  • explain the B-method or other used method,
  • understand and independently write model-based formal specifications,
  • independently carry out formal development of programs with tool support.

Content

Overview of specification techniques. Model-based specification. The B specification notation or similar notation. The program development process. Verification and validation. Simulation and other methods to validate specifications. Implementation models. Overview of axiomatic semantics. Invariants. Weakest preconditions. Verification by refinement. The B-method or similar method. Proof obligations. Proof techniques. Tools for formal software development.

Instruction

Lectures and seminars. During the course, students will carry out a program development project including writing a formal specification and developing provably correct program code.

Assessment

Seminars (3 ECTS credits) and the project (7 ECTS credits).

If there are special reasons for doing so, an examiner may make an exception from the method of assessment indicated and allow a student to be assessed by another method. An example of special reasons might be a certificate regarding special pedagogical support from the disability coordinator of the university.

FOLLOW UPPSALA UNIVERSITY ON

facebook
instagram
twitter
youtube
linkedin