| Code |
14466
|
| Year |
1
|
| Semester |
S2
|
| ECTS Credits |
6
|
| Workload |
PL(30H)/T(30H)
|
| Scientific area |
Informatics
|
|
Entry requirements |
N/A
|
|
Learning outcomes |
The general objectives are
• Understand the life cycle of secure and reliable software systems, from specification to verification, using techniques based on mathematical formalisms (formal methods).
• Learn about modern formal methods and techniques, when to use them, and which are most appropriate for each phase of secure and reliable software systems.
• Apply formal methods and techniques to the specification and verification of secure and reliable software systems.
|
|
Syllabus |
• Introduction to specification and programming languages for building secure and reliable software
• Logics for formal specification: Propositional logic, first-order logic and temporal logic
• Automatic proof techniques: SAT solving for propositional logic, SMT solving for first-order logic and theories, Bounded model-checking via SAT for temporal logic
• Program specification: Domain languages for behavioral specification, execution safety properties and functional properties, contract-based specification
• Static program verification: verification conditions for programs with contracts
• Dynamic program verification: runtime monitoring with contracts
• Introduction to formal methods for cyber-physical systems
|
|
Main Bibliography |
Michael Huth & Mark Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press; 2nd edition (2004).
Aaron R. Bradley & Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer (2007).
J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer (2011).
|
|
Teaching Methodologies and Assessment Criteria |
To assess the acquired competencies, the teaching-learning activities will evaluate the understanding of the theoretical concepts presented and the ability to apply them in practice. This assessment will be carried out through a written exam and a continuous assessment based on practical exercises.
NF = Final grade
NCP = Grade for the practical component (assessment of exercises)
NCT = Grade for the theoretical component (written exam)
NF = If (NCT >= 6 and NCP >= 6) then (NCT + NCP)/2 otherwise Fail/Not Admitted
|
|
Language |
Portuguese. Tutorial support is available in English.
|