Teaching GuideTerm Faculty of Computer Science |
Grao en Enxeñaría Informática |
![]() |
![]() |
![]() |
|
|
|
Identifying Data | 2024/25 | |||||||||||||
Subject | Software Verification and Validation | Code | 614G01225 | |||||||||||
Study programme |
|
|||||||||||||
Descriptors | Cycle | Period | Year | Type | Credits | |||||||||
Graduate | 2nd four-month period |
Fourth | Obligatory | 6 | ||||||||||
|
Topic | Sub-topic |
Part I: Software Testing |
I.1 Test specification, design, and execution I1.1. Levels and types of tests I1.2. Properties and traceability of requirements I.2 Test management: planning, assessment, metrics and reviews |
Part II: Formal methods and automatic reasoning |
II.1 Introduction: natural deduction and calculus of sequences II.2 Automatic proof using PVS II.3 What is a theorem prover and what is it used for? II.4 PVS specification language: types, expressions, theories, subtyping II.5 PVS prover: tactics, recursion, ecuational reasoning |
Part III: Model checking | III.1 Introduction to modal temporal logic III.2 Properties specification: deadlocks, safety, liveness, fairness III.3 How a model checker works III.4 Introduction to the use of a model checking tool |
|