The University of Southampton
Courses

COMP6210 Automated Software Verification

Module Overview

This module aims to introduce the area of software verification. A range of approaches will be covered. The use of specification languages, including logics, and the use of tools to support verification will be explored. The module will provide practical experience in using modern verification tools as well as covering some of the theory underpinning the correctness of these tools. The module is optional but MSc Software Engineers must choose this module and/or Automated Code Generation. The pre-requisite knowledge is basic familiarity with discrete mathematics and first-order logics.

Aims and Objectives

Module Aims

To introduce the area of software verification

Learning Outcomes

Knowledge and Understanding

Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:

  • The role of specification in formal verification
  • The theory underpinning explicit state, bounded and symbolic model checking
Subject Specific Practical Skills

Having successfully completed this module you will be able to:

  • Specify correctness conditions for software verification
  • Use at least two software verification tools proficiently

Syllabus

- Different approaches to software verification - Specification methods and logics - Software model checking - Explicit state model checking - Symbolic model checking - Bounded model checking - Software verification tools (including tools such as SPIN, JPF, CMBC, ESBMC, JML, SPEC#, DAFNY)

Learning and Teaching

TypeHours
Tutorial12
Completion of assessment task13
Lecture36
Revision10
Follow-up work18
Preparation for scheduled sessions18
Wider reading or practice43
Total study time150

Assessment

Summative

MethodPercentage contribution
Exam  (2 hours) 70%
Exercise 15%
Exercise 5%
Exercise 10%

Referral

MethodPercentage contribution
Exam  (2 hours) 100%

Repeat Information

Repeat type: Internal & External

Linked modules

Prerequisites: ELEC1204 or COMP1206

Share this module Facebook Google+ Twitter Weibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×