Syllabus for Provably Correct Software

Bevisbart korrekt programvara

A revised version of the syllabus is available.

Syllabus

  • 7.5 credits
  • Course code: 1DL017
  • 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)
  • Established: 2007-03-15
  • Established by: The Faculty Board of Science and Technology
  • Applies from: week 27, 2007
  • Entry requirements: BSc including Programming Methodology DV1, Algebra DV1, Logic and Proof Techniques DV1, Algorithms and Data Structures DV1, Programming Theory (or equivalent courses). Semantics and Principles of Programming Languages DV1 is recommended.
  • Responsible department: Department of Information Technology

Learning outcomes

In order to pass, the student must 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 (4.5 ECTS credits).

Syllabus Revisions

Reading list

Reading list

Applies from: week 27, 2007

Print syllabus and reading list
Print