Code: | CC4008 | Acronym: | CC4008 | Level: | 400 |
Keywords | |
---|---|
Classification | Keyword |
OFICIAL | Computer Science |
Active? | Yes |
Web Page: | http://www.dcc.fc.up.pt/~nam/web/Teaching/vfs18/index.html |
Responsible unit: | Department of Computer Science |
Course/CS Responsible: | Master in Computer Science |
Acronym | No. of Students | Study Plan | Curricular Years | Credits UCN | Credits ECTS | Contact hours | Total Time |
---|---|---|---|---|---|---|---|
M:CC | 4 | Study plan since 2014/2015 | 1 | - | 6 | 42 | 162 |
MI:ERS | 19 | Plano Oficial desde ano letivo 2014 | 4 | - | 6 | 42 | 162 |
To understand current trends in Program Verification techniques and approaches, to the certification of program properties, namely model checking and deductive methods.
Students should:
-to understand the importance of logic and formal systems for software engineering;
-to be able to model simple computer systems and to specify properties using temporal logics;
-to annotate programs to ensure safety and functional properties;
- Model checking of reactive systems
Modelling of parallel systemsL transition systems and concurrency. Linear time properties. Temporal logics: linear (LTL) and branching (CTL); model checkers; Symbolic model checking: BDDs and OBDDs
Automata based model checking algorithms.
- Program verification
Partial and total correctness calculus (Hoare logics). Verification condition generators. Tools for the specification , verification and certification of imperativ programs
designation | Weight (%) |
---|---|
Exame | 40,00 |
Teste | 40,00 |
Trabalho laboratorial | 20,00 |
Total: | 100,00 |
designation | Time (hours) |
---|---|
Estudo autónomo | 50,00 |
Frequência das aulas | 50,00 |
Total: | 100,00 |