Automated Software Verification

Learning Outcomes

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

Knowledge and Understanding

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

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

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

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

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.

Summative

This is how we’ll formally assess what you have learned in this module.

Referral

This is how we’ll assess you if you don’t meet the criteria to pass this module.

Repeat

An internal repeat is where you take all of your modules again, including any you passed. An external repeat is where you only re-take the modules you failed.