Segurança e Fiabilidade de Software

Código:
17908
Ano:
1
Semestre:
S1
Créditos ECTS:
6
Carga Horária:
PL(30H)/T(30H)
Área Científica:
Informática
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).
Language:
Portuguese. Tutorial support is available in English.
Esta informação promove os seguintes Objetivos de Desenvolvimento Sustentável da ONU:
Garantir o acesso à educação inclusiva, de qualidade e equitativa, e promover oportunidades de aprendizagem ao longo da vida para todos