Teaching GuideTerm Faculty of Computer Science |
Grao en Enxeñaría Informática |
![]() |
![]() |
![]() |
|
|
|
Identifying Data | 2024/25 | |||||||||||||
Subject | Software Verification and Validation | Code | 614G01053 | |||||||||||
Study programme |
|
|||||||||||||
Descriptors | Cycle | Period | Year | Type | Credits | |||||||||
Graduate | 1st four-month period |
Fourth | Optional | 6 | ||||||||||
|
Topic | Sub-topic |
Part I: Software Validation |
I.1 Test specification, design and execution I1.1. Levels and types of tests I1.2. Properties and traceability of requirements I1.3. Automation 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 proofs 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 |
|