Skip to main navigationSkip to main content
The University of Southampton
Courses

COMP6210 Automated Software Verification

Module Overview

This module aims to train students in both the principles and the practice of software verification. A range of verification approaches, including both testing and formal verification, will be covered. The use of logic as a specification language for programs will be explored. In addition to covering the key techniques for software verification, the module will provide practical experience in using state of the art verification tools.

Aims and Objectives

Learning Outcomes

Knowledge and Understanding

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

  • A range of testing and verification approaches applicable to software systems
  • The use of logic as a specification language for software correctness
Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

  • Apply automated verification techniques to software
  • Assess the limitations of current verification techniques and tools
Subject Specific Practical Skills

Having successfully completed this module you will be able to:

  • Select appropriate verification tools to analyse and verify small-scale systems

Syllabus

Software testing 1. Types of testing 2. Black-box testing 3. Test coverage and structural testing 4. Regression testing 5. Automated test case generation Formal verification 1. Approaches to modelling software 2. Property specification using temporal logic 3. Model checking 4. Symbolic execution

Learning and Teaching

Teaching and learning methods

The module uses lectures to present the material and tutorials to enhance the understanding of various verification techniques and demonstrate the use of verification tools.

TypeHours
Tutorial12
Revision15
Wider reading or practice6
Independent Study18
Lecture36
Preparation for scheduled sessions18
Completion of assessment task45
Total study time150

Assessment

Summative

MethodPercentage contribution
Continuous Assessment  35%
Final Assessment  65%

Repeat

MethodPercentage contribution
Set Task  (2 hours) 100%

Referral

MethodPercentage contribution
Set Task  (2 hours) 100%

Repeat Information

Repeat type: Internal & External

Share this module Share this on Facebook Share this on Twitter Share this on Weibo
Privacy Settings