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
Follow-up work18
Completion of assessment task13
Preparation for scheduled sessions18
Lecture36
Revision10
Tutorial12
Wider reading or practice43
Total study time150

Assessment

Summative

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

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.

×