| Code |
14466
|
| Year |
1
|
| Semester |
S2
|
| ECTS Credits |
6
|
| Workload |
PL(30H)/T(30H)
|
| Scientific area |
Informatics
|
|
Entry requirements |
Does not have.
|
|
Learning outcomes |
The objectives are:
• understand and master the development life cycle of secure and reliable IT systems based on Formal Methods.
• Know the existing formal methods, know when they should be applied and which are the most appropriate in each case.
• Apply the formal methods of specification, modelling and verification in the development of secure and reliable computer systems.
• Understand, be able to select but also design program static analyses methods and tools.
|
|
Syllabus |
1. Formal methods in software engineering
2. Data Flow Analysis
3. Path Sensitivity, interprocedural analysis and control flow analysis
4. Timed (timed) logic, timed model checking,
5. Model Checking with UPPAAL.
6. Operational semantics for verification
7. Denotational, trace semantics
8. Axiomatic semantics, Hoare Logic, WPC and VCGEN
10. Theory of Types and Curry-Howard Isomorphism
11. Formal verification of C programs with Frama-C
|
|
Main Bibliography |
J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first edition, 307 p. 52 illus, 2011.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004.
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.
|
|
Teaching Methodologies and Assessment Criteria |
Teaching method are theoretical lessons, 2 hours each week and also a practical session of two hours
|
|
Language |
Portuguese. Tutorial support is available in English.
|