In the first opportunity, students that do not reach the minimum in the objective test, will receive the mark they obtain in that objective test.

In the second opportunity, the objective test will have a weight of 80% for those students which continuous and lab evaluation sums up less than 1 point, in order to guarantee their right to pass the subject.

In compliance with the academic rules at UDC that apply to part-time students, physical presence in the classroom/laboratory will not be regarded as a qualification element. That is to say, students may officially apply to be dismissed from attending lectures and laboratory practices. All in all, part-time students will still need to comply with deadlines established for supervised projects and laboratory projects.

Likewise, as stated in the different regulations applicable to university teaching, the incorporation of the gender perspective in this subject will be enforced by using non-sexist language and encouraging the intervention, during the master sessions, of women and men in a balanced way. We will work to identify and modify prejudices and sexist attitudes, and we will influence the environment to modify them and promote values of respect and equality. Finally, if situations of gender-based discrimination are detected, actions and measures will be proposed to correct them.

Learning outcomes	Study programme competences
Ability to identify and analise problems, and to design, develop, implement, validate and document software solutions on the basis of an deep understanding and knowledge of modern theories, models and techniques.	A28	B1 B3	C2 C3 C6 C7 C8

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

Methodologies / tests	Competencies	Ordinary class hours	Student’s personal work hours	Total hours
Guest lecture / keynote speech	B3 C2 C7 C8	21	26.25	47.25
Laboratory practice	A28 B1 B3 C2 C3 C6	21	42	63
Objective test	B1 B3 C6	3	31.5	34.5

Personalized attention		5.25	0	5.25

(*)The information in the planning table is for guidance only and does not take into account the heterogeneity of the students.

Methodologies	Description
Guest lecture / keynote speech	Master class where the theoretical contents of the study programme are presented.
Laboratory practice	Hands-on work sessions in the lab.
Objective test	Written test.

Methodologies	Competencies	Description	Qualification
Objective test	B1 B3 C6	Written test, up to 4 points in the final score. A minimum of 2 points is required to pass.	40
Laboratory practice	A28 B1 B3 C2 C3 C6	Hand in and presentation of hands-on student assignments, up to 6 points in the final score (2 points per content topic). These are not compulsory to pass.	60

Assessment comments
In the first opportunity, students that do not reach the minimum in the objective test, will receive the mark they obtain in that objective test. In the second opportunity, the objective test will have a weight of 80% for those students which continuous and lab evaluation sums up less than 1 point, in order to guarantee their right to pass the subject. In compliance with the academic rules at UDC that apply to part-time students, physical presence in the classroom/laboratory will not be regarded as a qualification element. That is to say, students may officially apply to be dismissed from attending lectures and laboratory practices. All in all, part-time students will still need to comply with deadlines established for supervised projects and laboratory projects. Likewise, as stated in the different regulations applicable to university teaching, the incorporation of the gender perspective in this subject will be enforced by using non-sexist language and encouraging the intervention, during the master sessions, of women and men in a balanced way. We will work to identify and modify prejudices and sexist attitudes, and we will influence the environment to modify them and promote values of respect and equality. Finally, if situations of gender-based discrimination are detected, actions and measures will be proposed to correct them.

Basic	Crispin Lisa, Gregory Janet (2008). Agile Testing: A Practical Guide for Testers and Agile Teams. Addison-Wesley Maurício Aniche (2022). Effective software testing. Manning Gayathri Mohan (2022). Full Stack Testing. O'Reilly Media, Inc. Mordechai Ben-Ari (2012). Mathematical Logic for Computer Science. Springer Mordechai Ben-Ari (2001). Mathematical Logic for Computer Science. Springer Charity Majors, Liz Fong-Jones, George Miranda (2022). Observability Engineering. O'Reilly Media, Inc. Fred Hébert (2019). Property-based testing with PropEr, Erlang, and Elixir : find bugs before your users do. The Pragmatic Bookshelf Brian Okken (2022). Python testing with pytest. The Pragmetic Programmers Kent Beck (2002). Test Driven Development (By Example). Addison-Wesley Gerard J. Holzmann (2003). The SPIN model checker: primer and reference manual. Addison-Wesley Zohar Manna and Amir Pnueli (1995). The Temporal Logic of Reactive and Concurrent Systems. Safety. Springer Zohar Manna and Amir Pnueli (1991). The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer

Complementary

Other comments