| Code |
15646
|
| Year |
1
|
| Semester |
S2
|
| ECTS Credits |
6
|
| Workload |
PL(30H)/T(30H)
|
| Scientific area |
Informatics
|
|
Entry requirements |
Does not have.
|
|
Learning outcomes |
The general 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 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. Orders, lattices and the monotone framework
3. Data Flow Analysis
4. Path Sensitivity, interprocedural analysis and control flow analysis
5. Pointer analysis
6. Operational semantics for verification
7. Denotational, trace semantics
8. Axiomatic semantics, Hoare Logic, WPC and VCGEN
9. Deductive program verification on Why3
10. Theory of Types and Curry-Howard Isomorphism
11. Formal verification and evidence of COQ programs
12. Timed (timed) logic, timed model checking,
13. Model Checking with UPPAAL.
|
|
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 |
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.
|