| 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 |
The face-to-face classes are divided into two categories
1. Theoretical classes where the theoretical concepts, the mathematical models specific to software construction / validation / analysis, the underlying algorithms, but also the capacitive technologies to the production of reliable and safe software are exposed.
2. Practical classes with application of program specification and verification techniques
In order to evaluate the acquired competences, the activities of Teaching-Learning will evaluate the understanding of the exposed theoretical concepts and the ability to put such concepts in practice. Thus, it will be carried out by a written test and by continuous evaluation based on practical exercises.
NF = Final grade
NCP = Grade for the practical component
NCT = grade for the theoretical component (written test) NF = if (NCT> = 6) then (NCT + NCP) / 2 else “Fail”
|
|
Language |
Portuguese. Tutorial support is available in English.
|